Documentation

Lean 4 Proof

theorem sectorMultiplier_eq_cesMultiplier (e : NSectorEconomy N) (n : Fin N) :
    sectorMultiplier e n = cesMultiplier (e.J n) (e.ρ n) (e.d_sq n) := by
  rfl

Dependency Graph

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:79

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy

In the same file