Documentation

Lean 4 Proof

theorem effectiveSectorMultiplier_nonneg (e : NSectorEconomy N) (n : Fin N) :
    0 ≤ effectiveSectorMultiplier e n := by
  unfold effectiveSectorMultiplier
  exact mul_nonneg (sectorEffectiveCurvature_nonneg e n) (le_of_lt (e.hd n))

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:89

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy

In the same file