Documentation

Lean 4 Proof

theorem efficiency_volatility_tradeoff (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 ∧
    sectorCurvature e m < sectorCurvature e n :=
  ⟨multiplier_rho_ordering e hJ_eq hd_eq hρ,
   by simp only [sectorCurvature]; rw [← hJ_eq];
      exact curvatureK_decreasing_in_rho (e.hJ n) hρ⟩

Dependency Graph

Location

thesis/CESProofs/Dynamics/MultiplierCycles.lean:140

Module Section

Multiplier-Cycle Duality in a Multi-Sector Economy

In the same file