Documentation

Lean 4 Proof

theorem valueFunction_at_one {ρ c : ℝ} :
    valueFunction 1 ρ c = 0 := by
  simp [valueFunction, curvatureKReal_one]

Dependency Graph

Location

thesis/CESProofs/EntryExit/Calculus.lean:106

Module Section

Paper 1c: Formal Calculus on K(J) and V(J)

In the same file