Documentation

Lean 4 Proof

theorem recession_dual_degradation {J : ℕ} (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {T1 T2 Tstar : ℝ} (hTs : 0 < Tstar) (h : T1 ≤ T2) :
    effectiveCurvatureKeff J ρ T2 Tstar ^ 2 ≤
    effectiveCurvatureKeff J ρ T1 Tstar ^ 2 :=
  bilateral_Keff_sq_decreasing hJ hρ hTs h

Dependency Graph

Location

thesis/CESProofs/Potential/MacroApplications.lean:211

Module Section

Macroeconomic Applications of the CES Potential

In the same file