Documentation

Lean 4 Proof

theorem fiscal_multiplier_heterogeneity {J : ℕ} (hJ : 2 ≤ J)
    {ρ1 ρ2 : ℝ} (hρ1 : ρ1 < 1) (hρ2 : ρ2 < 1) (hρ : ρ1 < ρ2)
    {T Tstar d_sq : ℝ} (_hTs : 0 < Tstar) (_hT : 0 ≤ T) (hd : 0 ≤ d_sq) :
    effectiveMultiplier J ρ2 T Tstar d_sq ≤ effectiveMultiplier J ρ1 T Tstar d_sq := by
  simp only [effectiveMultiplier]
  exact mul_le_mul_of_nonneg_right
    (complementary_goods_higher_Keff hJ hρ1 hρ2 hρ _hTs _hT) hd

Dependency Graph

Location

thesis/CESProofs/Potential/MacroApplications.lean:100

Module Section

Macroeconomic Applications of the CES Potential

In the same file