Documentation

Lean 4 Proof

theorem hasDerivAt_valueFunction {J ρ c : ℝ} (hJ : 0 < J) :
    HasDerivAt (fun x => valueFunction x ρ c) (valueFunctionDeriv J ρ c) J := by
  simp only [valueFunction, valueFunctionDeriv]
  exact (hasDerivAt_curvatureK_real (ne_of_gt hJ)).mul (hasDerivAt_perCapitaBenefit hJ)

Dependency Graph

Used by

Location

thesis/CESProofs/EntryExit/Calculus.lean:80

Module Section

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

In the same file