Documentation

Lean 4 Proof

theorem multisector_stagflation (e : NSectorEconomy N) (n : Fin N)
    {T2 : ℝ} (hT2 : e.T n ≤ T2) :
    -- (a) Effective curvature decreases (output falls)
    effectiveCurvatureKeff (e.J n) (e.ρ n) T2 (sectorCriticalFriction e n) ≤
      sectorEffectiveCurvature e n ∧
    -- (b) Allocation distortion increases (prices rise)
    sectorAllocationDistortion e n ≤
      allocationDistortion T2 (sectorCriticalFriction e n) := by
  simp only [sectorEffectiveCurvature, sectorAllocationDistortion]
  exact ⟨bilateral_Keff_decreasing (e.hJ n) (e.hρ n)
           (sectorCriticalFriction_pos e n) hT2,
         allocationDistortion_monotone (sectorCriticalFriction_pos e n) hT2⟩

Dependency Graph

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:171

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy

In the same file