Documentation

Lean 4 Proof

def concentrationWelfareCost (ρ : ℝ) (N : ℕ) : ℝ :=
  (1 - ρ) * (1 - 1 / ↑N)

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:88

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file