Documentation

Lean 4 Proof

theorem bilateral_Keff_sq_decreasing {J : ℕ} (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    {T1 T2 Tstar : ℝ} (hTs : 0 < Tstar) (h : T1 ≤ T2) :
    effectiveCurvatureKeff J ρ T2 Tstar ^ 2 ≤
    effectiveCurvatureKeff J ρ T1 Tstar ^ 2 := by
  apply pow_le_pow_left₀ (effectiveCurvatureKeff_nonneg hJ hρ T2 Tstar)
    (bilateral_Keff_decreasing hJ hρ hTs h)

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/BilateralTrade.lean:66

Module Section

Bilateral Trade Collapse Ordering

In the same file