Documentation

Lean 4 Proof

def aggregateOscillationEnergy (e : NSectorEconomy N) (ξ : Fin N → ℝ) : ℝ :=
  oscillationEnergy (fun n => sectorEffectiveCurvature e n) ξ

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:268

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy

In the same file