Documentation

Lean 4 Proof

theorem complementarity_paradox_benefit {J ρ₁ ρ₂ : ℝ}
    (hJ : 1 < J) (hρ : ρ₁ < ρ₂) :
    curvatureKReal J ρ₂ < curvatureKReal J ρ₁ := by
  simp only [curvatureKReal]
  have hJpos : 0 < J := by linarith
  -- (1-ρ₂)(J-1)/J < (1-ρ₁)(J-1)/J because (1-ρ₂) < (1-ρ₁) and (J-1)/J > 0
  rw [div_lt_div_iff₀ hJpos hJpos]
  have hJm1 : 0 < J - 1 := by linarith
  nlinarith [mul_pos hJm1 hJpos]

Dependency Graph

Location

thesis/CESProofs/EntryExit/Welfare.lean:104

Module Section

Paper 1c, Section 4: Welfare and Coordination Failure

In the same file