Documentation

Lean 4 Proof

theorem bilateral_Keff_strict {J : ℕ} (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {T1 T2 Tstar : ℝ} (hTs : 0 < Tstar) (h : T1 < T2) (hT2 : T2 < Tstar) :
    effectiveCurvatureKeff J ρ T2 Tstar < effectiveCurvatureKeff J ρ T1 Tstar := by
  simp only [effectiveCurvatureKeff]
  apply mul_lt_mul_of_pos_left _ (curvatureK_pos hJ hρ)
  -- Need: max 0 (1 - T₂/T*) < max 0 (1 - T₁/T*)
  have hm1 : 0 < 1 - T1 / Tstar := by
    rw [sub_pos, div_lt_one hTs]; linarith
  have hm2 : 0 < 1 - T2 / Tstar := by
    rw [sub_pos, div_lt_one hTs]; exact hT2
  rw [max_eq_right (le_of_lt hm1), max_eq_right (le_of_lt hm2)]
  have : T1 / Tstar < T2 / Tstar := div_lt_div_of_pos_right h hTs
  linarith

Dependency Graph

Location

thesis/CESProofs/Potential/BilateralTrade.lean:44

Module Section

Bilateral Trade Collapse Ordering

In the same file