Documentation

Lean 4 Proof

theorem crisis_zeroes_multiplier (e : NSectorEconomy N) (n : Fin N)
    (hT : sectorCriticalFriction e n ≤ e.T n) :
    effectiveSectorMultiplier e n = 0 := by
  simp only [effectiveSectorMultiplier]
  rw [weakest_sector_crisis e n hT, zero_mul]

Dependency Graph

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:231

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy

In the same file