Documentation

Lean 4 Proof

theorem stagflation {J : ℕ} (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {T1 T2 Tstar d_sq : ℝ} (hTs : 0 < Tstar) (h : T1 ≤ T2) (hd : 0 ≤ d_sq) :
    -- (a) Output falls: effective multiplier decreases
    effectiveMultiplier J ρ T2 Tstar d_sq ≤ effectiveMultiplier J ρ T1 Tstar d_sq ∧
    -- (b) Prices rise: allocation distortion increases
    allocationDistortion T1 Tstar ≤ allocationDistortion T2 Tstar :=
  ⟨effectiveMultiplier_decreasing_in_T hJ hρ hTs h hd,
   allocationDistortion_monotone hTs h⟩

Dependency Graph

Location

thesis/CESProofs/Potential/MacroApplications.lean:195

Module Section

Macroeconomic Applications of the CES Potential

In the same file