Documentation

Lean 4 Proof

theorem sectorCurvature_pos (e : NSectorEconomy N) (n : Fin N) :
    0 < sectorCurvature e n := by
  unfold sectorCurvature
  exact curvatureK_pos (e.hJ n) (e.hρ n)

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:38

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy

In the same file