Documentation

Lean 4 Proof

theorem shockAmplification_symm (e : NSectorEconomy N) (n m : Fin N) :
    shockAmplification e n m = shockAmplification e m n := by
  simp only [shockAmplification]; ring

Dependency Graph

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:196

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy

In the same file