Documentation

Lean 4 Proof

theorem aggregateOscillationEnergy_nonneg (e : NSectorEconomy N)
    (ξ : Fin N → ℝ) :
    0 ≤ aggregateOscillationEnergy e ξ := by
  unfold aggregateOscillationEnergy
  exact oscillationEnergy_nonneg (fun n => sectorEffectiveCurvature_nonneg e n) ξ

Dependency Graph

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:272

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy

In the same file