Documentation

Lean 4 Proof

theorem sectorEffectiveCurvature_nonneg (e : NSectorEconomy N) (n : Fin N) :
    0 ≤ sectorEffectiveCurvature e n := by
  unfold sectorEffectiveCurvature
  exact effectiveCurvatureKeff_nonneg (e.hJ n) (e.hρ n) (e.T n)
    (sectorCriticalFriction e n)

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:56

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy

In the same file