Documentation

Lean 4 Proof

theorem curvature_gain_formula {ρ : ℝ} {N : ℕ} :
    concentrationWelfareCost ρ N = (1 - ρ) * (1 - bequestHerfindahl N) := by
  simp only [concentrationWelfareCost, bequestHerfindahl]

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:364

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file