Documentation

Lean 4 Proof

theorem dispersion_raises_curvature {ρ : ℝ} {N₁ N₂ : ℕ}
    (hρ : ρ < 1) (hN₁ : 0 < N₁) (_hN₂ : 0 < N₂) (h : N₁ < N₂) :
    concentrationWelfareCost ρ N₁ < concentrationWelfareCost ρ N₂ := by
  simp only [concentrationWelfareCost]
  apply mul_lt_mul_of_pos_left _ (by linarith : (0 : ℝ) < 1 - ρ)
  -- Need: 1 - 1/N₁ < 1 - 1/N₂, i.e., 1/N₂ < 1/N₁
  have h_herf := more_heirs_lower_herfindahl hN₁ h
  simp only [bequestHerfindahl] at h_herf
  linarith

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:163

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file