Documentation

Lean 4 Proof

theorem shockAmplification_nonneg (e : NSectorEconomy N) (n m : Fin N) :
    0 ≤ shockAmplification e n m := by
  unfold shockAmplification
  exact mul_nonneg (sectorEffectiveCurvature_nonneg e n)
                   (sectorEffectiveCurvature_nonneg e m)

Dependency Graph

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:201

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy

In the same file