Documentation

Lean 4 Proof

theorem crisis_destroys_amplification (e : NSectorEconomy N) {n : Fin N}
    (hT : sectorCriticalFriction e n ≤ e.T n) (m : Fin N) :
    shockAmplification e n m = 0 := by
  simp only [shockAmplification]
  rw [weakest_sector_crisis e n hT, zero_mul]

Dependency Graph

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:223

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy

In the same file