Documentation

Lean 4 Proof

theorem bilateral_Keff_decreasing {J : ℕ} (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {T1 T2 Tstar : ℝ} (hTs : 0 < Tstar) (h : T1 ≤ T2) :
    effectiveCurvatureKeff J ρ T2 Tstar ≤ effectiveCurvatureKeff J ρ T1 Tstar := by
  simp only [effectiveCurvatureKeff]
  exact mul_le_mul_of_nonneg_left (degradation_monotone hTs h)
    (le_of_lt (curvatureK_pos hJ hρ))

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/BilateralTrade.lean:34

Module Section

Bilateral Trade Collapse Ordering

In the same file