Documentation

Lean 4 Proof

theorem complementary_goods_more_fragile {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) :
    criticalFriction J rho1 c d_sq < criticalFriction J rho2 c d_sq := by
  simp only [criticalFriction]
  have hJ_pos : (0 : ℝ) < ↑J := by exact_mod_cast (show 0 < J by omega)
  have hJm1 : (0 : ℝ) < ↑J - 1 := by
    have : (2 : ℝ) ≤ ↑J := by exact_mod_cast hJ
    linarith
  -- Numerator: 2 * (↑J - 1) * c ^ 2 * d_sq > 0
  have hnum : 0 < 2 * (↑J - 1) * c ^ 2 * d_sq := by positivity
  -- K(rho1) > K(rho2) > 0
  have hK1 : 0 < curvatureK J rho1 := curvatureK_pos hJ hrho1
  have hK_lt : curvatureK J rho2 < curvatureK J rho1 :=
    curvatureK_decreasing_in_rho hJ hrho
  -- numerator / K1 < numerator / K2 since K1 > K2 > 0
  have hK2 : 0 < curvatureK J rho2 := curvatureK_pos hJ _hrho2
  exact div_lt_div_of_pos_left hnum hK2 hK_lt

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/BilateralTrade.lean:118

Module Section

Bilateral Trade Collapse Ordering

In the same file