Documentation

Lean 4 Proof

theorem highest_friction_pair_fails_first {J : ℕ} (hJ : 2 ≤ J)
    {ρ : ℝ} (hρ : ρ < 1)
    {T1 T2 Tstar : ℝ} (hTs : 0 < Tstar)
    (hT1_nn : 0 ≤ T1) (hT1 : T1 < Tstar) (hT2 : Tstar ≤ T2) :
    effectiveCurvatureKeff J ρ T2 Tstar = 0 ∧
    0 < effectiveCurvatureKeff J ρ T1 Tstar := by
  constructor
  · exact effectiveCurvatureKeff_above_critical J ρ T2 Tstar hTs hT2
  · exact effectiveCurvatureKeff_pos hJ hρ hT1_nn hTs hT1

Dependency Graph

Location

thesis/CESProofs/Potential/BilateralTrade.lean:165

Module Section

Bilateral Trade Collapse Ordering

In the same file