Documentation

Lean 4 Proof

theorem sectorMultiplier_pos (e : NSectorEconomy N) (n : Fin N) :
    0 < sectorMultiplier e n := by
  unfold sectorMultiplier
  exact mul_pos (sectorCurvature_pos e n) (e.hd n)

Dependency Graph

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:73

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy

In the same file