Documentation

Lean 4 Proof

theorem multiplier_rho_ordering (e : NSectorEconomy N) {n m : Fin N}
    (hJ_eq : e.J n = e.J m) (hd_eq : e.d_sq n = e.d_sq m)
    (hρ : e.ρ n < e.ρ m) :
    sectorMultiplier e m < sectorMultiplier e n := by
  simp only [sectorMultiplier, sectorCurvature]
  rw [← hJ_eq, ← hd_eq]
  exact mul_lt_mul_of_pos_right
    (curvatureK_decreasing_in_rho (e.hJ n) hρ) (e.hd n)

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:127

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy

In the same file