Documentation

Lean 4 Proof

theorem incentive_compatible {τ_R W E₀ : ℝ} {N_conc N_disp : ℕ}
    (hτ : 0 < τ_R) (hW : 0 < W)
    (h_conc : E₀ < perHeirWealth W N_conc)
    (h_disp : perHeirWealth W N_disp ≤ E₀) :
    -- Tax paid under dispersion < tax paid under concentration
    dispersionTaxRevenue τ_R W E₀ N_disp < dispersionTaxRevenue τ_R W E₀ N_conc := by
  rw [zero_tax_when_dispersed h_disp]
  simp only [dispersionTaxRevenue, if_neg (not_le.mpr h_conc)]
  exact mul_pos hτ hW

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:328

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file