Documentation

Lean 4 Proof

theorem effectiveMultiplier_decreasing_in_T {J : ℕ} (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {T1 T2 Tstar d_sq : ℝ} (hTs : 0 < Tstar) (h : T1 ≤ T2) (hd : 0 ≤ d_sq) :
    effectiveMultiplier J ρ T2 Tstar d_sq ≤ effectiveMultiplier J ρ T1 Tstar d_sq := by
  simp only [effectiveMultiplier]
  exact mul_le_mul_of_nonneg_right (bilateral_Keff_decreasing hJ hρ hTs h) hd

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/MacroApplications.lean:80

Module Section

Macroeconomic Applications of the CES Potential

In the same file