Effective Sector Multiplier

def proved Dynamics & Crises

Documentation

Lean 4 Proof

def effectiveSectorMultiplier (e : NSectorEconomy N) (n : Fin N) : ℝ :=
  sectorEffectiveCurvature e n * e.d_sq n

Dependency Graph

Used by

crisis_zeroes_multiplier aggregateEffectiveMultiplier effectiveSectorMultiplier_nonneg effectiveSectorMultiplier_le

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:85

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy