Documentation

Lean 4 Proof

theorem effectiveMultiplier_zero_at_critical {J : ℕ} {ρ : ℝ}
    {T Tstar d_sq : ℝ} (hTs : 0 < Tstar) (hT : Tstar ≤ T) :
    effectiveMultiplier J ρ T Tstar d_sq = 0 := by
  simp only [effectiveMultiplier]
  rw [effectiveCurvatureKeff_above_critical J ρ T Tstar hTs hT, zero_mul]

Dependency Graph

Location

thesis/CESProofs/Potential/MacroApplications.lean:89

Module Section

Macroeconomic Applications of the CES Potential

In the same file