Documentation

Lean 4 Proof

theorem complementary_goods_higher_Keff {J : ℕ} (hJ : 2 ≤ J)
    {rho1 rho2 : ℝ} (_hrho1 : rho1 < 1) (_hrho2 : rho2 < 1)
    (hrho : rho1 < rho2)
    {T Tstar : ℝ} (_hTs : 0 < Tstar) (_hT : 0 ≤ T) :
    effectiveCurvatureKeff J rho2 T Tstar ≤
    effectiveCurvatureKeff J rho1 T Tstar := by
  simp only [effectiveCurvatureKeff]
  -- K(rho2) ≤ K(rho1) and degradation factor is the same for both
  apply mul_le_mul_of_nonneg_right
  · exact le_of_lt (curvatureK_decreasing_in_rho hJ hrho)
  · exact le_max_left 0 _

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/BilateralTrade.lean:145

Module Section

Bilateral Trade Collapse Ordering

In the same file