Documentation

Lean 4 Proof

def aggregateEffectiveMultiplier (e : NSectorEconomy N) : ℝ :=
  ∑ n : Fin N, effectiveSectorMultiplier e n

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:111

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy

In the same file