Documentation

Lean 4 Proof

theorem recession_depth_proportional_to_K {J : ℕ}
    {ρ : ℝ} {T1 T2 Tstar : ℝ} (hTs : 0 < Tstar)
    (hT1 : T1 < Tstar) (hT2 : T2 < Tstar) :
    effectiveCurvatureKeff J ρ T1 Tstar - effectiveCurvatureKeff J ρ T2 Tstar =
    curvatureK J ρ * (T2 - T1) / Tstar := by
  simp only [effectiveCurvatureKeff]
  have hm1 : 0 < 1 - T1 / Tstar := by rw [sub_pos, div_lt_one hTs]; exact hT1
  have hm2 : 0 < 1 - T2 / Tstar := by rw [sub_pos, div_lt_one hTs]; exact hT2
  rw [max_eq_right (le_of_lt hm1), max_eq_right (le_of_lt hm2)]
  have : Tstar ≠ 0 := ne_of_gt hTs
  field_simp
  ring

Dependency Graph

Location

thesis/CESProofs/Potential/MacroApplications.lean:120

Module Section

Macroeconomic Applications of the CES Potential

In the same file