Sector Multiplier

def proved Dynamics & Crises

Documentation

Lean 4 Proof

def sectorMultiplier (e : NSectorEconomy N) (n : Fin N) : ℝ :=
  sectorCurvature e n * e.d_sq n

Dependency Graph

Used by

sectorMultiplier_pos efficiency_volatility_tradeoff effectiveSectorMultiplier_le multiplier_rho_ordering sectorMultiplier_eq_cesMultiplier

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:69

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy