Documentation

Lean 4 Proof

theorem dispersion_dominance {ρ : ℝ} {N : ℕ} (hρ : ρ < 1) (hN : 2 ≤ N) :
    0 < concentrationWelfareCost ρ N := by
  simp only [concentrationWelfareCost]
  apply mul_pos (by linarith : (0 : ℝ) < 1 - ρ)
  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:185

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file