Documentation

Lean 4 Proof

theorem aggregateEffectiveMultiplier_nonneg (e : NSectorEconomy N) :
    0 ≤ aggregateEffectiveMultiplier e := by
  unfold aggregateEffectiveMultiplier
  exact Finset.sum_nonneg fun n _ => effectiveSectorMultiplier_nonneg e n

Dependency Graph

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:115

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy

In the same file