Documentation

Lean 4 Proof

theorem curvature_gain_increases_with_complementarity {ρ₁ ρ₂ : ℝ} {N : ℕ}
    (hN : 2 ≤ N) (h : ρ₁ < ρ₂) :
    concentrationWelfareCost ρ₂ N < concentrationWelfareCost ρ₁ N := by
  simp only [concentrationWelfareCost]
  apply mul_lt_mul_of_pos_right (by linarith)
  have hNpos : (0 : ℝ) < ↑N := by exact_mod_cast (by omega : 0 < N)
  have hNgt1 : (1 : ℝ) < ↑N := by exact_mod_cast (by omega : 1 < N)
  have : 1 / (↑N : ℝ) < 1 := by rw [div_lt_one hNpos]; exact hNgt1
  linarith

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:372

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file