Documentation

Lean 4 Proof

theorem efficiency_fragility_tradeoff {J : ℕ} (hJ : 2 ≤ J)
    {rho1 rho2 : ℝ} (hrho1 : rho1 < 1) (hrho2 : rho2 < 1)
    (hrho : rho1 < rho2)
    {c d_sq : ℝ} (hc : 0 < c) (hd : 0 < d_sq)
    {T Tstar : ℝ} (hTs : 0 < Tstar) (hT : 0 ≤ T) :
    -- More complementary goods have higher effective curvature...
    effectiveCurvatureKeff J rho2 T Tstar ≤
      effectiveCurvatureKeff J rho1 T Tstar ∧
    -- ...but lower critical friction (more fragile)
    criticalFriction J rho1 c d_sq < criticalFriction J rho2 c d_sq := by
  exact ⟨complementary_goods_higher_Keff hJ hrho1 hrho2 hrho hTs hT,
         complementary_goods_more_fragile hJ hrho1 hrho2 hrho hc hd⟩

Dependency Graph

Location

thesis/CESProofs/Potential/BilateralTrade.lean:183

Module Section

Bilateral Trade Collapse Ordering

In the same file