Documentation

Lean 4 Proof

theorem zero_tax_when_dispersed {τ_R W E₀ : ℝ} {N : ℕ}
    (h_dispersed : perHeirWealth W N ≤ E₀) :
    dispersionTaxRevenue τ_R W E₀ N = 0 := by
  simp only [dispersionTaxRevenue, if_pos h_dispersed]

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:123

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file