Documentation

Lean 4 Proof

def dispersionTaxRevenue (τ_R W E₀ : ℝ) (N : ℕ) : ℝ :=
  if perHeirWealth W N ≤ E₀ then 0 else τ_R * W

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:57

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file