Documentation

Lean 4 Proof

theorem effectiveSectorMultiplier_le (e : NSectorEconomy N) (n : Fin N) :
    effectiveSectorMultiplier e n ≤ sectorMultiplier e n := by
  simp only [effectiveSectorMultiplier, sectorMultiplier,
             sectorEffectiveCurvature, sectorCurvature]
  exact mul_le_mul_of_nonneg_right
    (effectiveCurvatureKeff_le_K (e.hJ n) (e.hρ n) (e.hT n)
      (sectorCriticalFriction_pos e n))
    (le_of_lt (e.hd n))

Dependency Graph

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:96

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy

In the same file