Documentation

Lean 4 Proof

theorem weakest_sector_crisis (e : NSectorEconomy N) (n : Fin N)
    (hT : sectorCriticalFriction e n ≤ e.T n) :
    sectorEffectiveCurvature e n = 0 := by
  simp only [sectorEffectiveCurvature]
  exact effectiveCurvatureKeff_above_critical _ _ _ _
    (sectorCriticalFriction_pos e n) hT

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:213

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy

In the same file