Documentation

Lean 4 Proof

theorem valueFunctionDeriv_pos {J ρ c : ℝ}
    (hJ : 1 < J) (hρ0 : 0 < ρ) (hρ1 : ρ < 1) (hc : 0 < c) :
    0 < valueFunctionDeriv J ρ c := by
  simp only [valueFunctionDeriv]
  have hJpos : 0 < J := by linarith
  apply add_pos
  · exact mul_pos (pigouvian_subsidy_pos hJpos hρ1) (perCapitaBenefit_pos hJpos hc)
  · apply mul_pos (curvatureKReal_pos hJ hρ1)
    apply mul_pos (mul_pos _ (rpow_pos_of_pos hJpos _)) hc
    rw [sub_pos, lt_div_iff₀ hρ0]; linarith

Dependency Graph

Used by

Location

thesis/CESProofs/EntryExit/Calculus.lean:94

Module Section

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

In the same file