Documentation

Lean 4 Proof

theorem K_increases_with_complementarity (hJ : 2 ≤ J) {ρ₁ ρ₂ : ℝ}
    (_hρ1 : ρ₁ < 1) (_hρ2 : ρ₂ < 1) (h12 : ρ₂ < ρ₁) :
    curvatureK J ρ₁ < curvatureK J ρ₂ := by
  simp only [curvatureK]
  apply div_lt_div_of_pos_right _ (by exact_mod_cast (show 0 < J by omega))
  apply mul_lt_mul_of_pos_right
  · linarith
  · have : (1 : ℝ) < ↑J := by exact_mod_cast (show 1 < J by omega)
    linarith

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/Welfare.lean:242

Module Section

Theorem 8, Corollary 6, Propositions 18-22:

In the same file