Documentation

Lean 4 Proof

theorem dispersion_revenue_nonneg {τ_R W E₀ : ℝ} {N : ℕ}
    (hτ : 0 ≤ τ_R) (hW : 0 ≤ W) :
    0 ≤ dispersionTaxRevenue τ_R W E₀ N := by
  simp only [dispersionTaxRevenue]
  split_ifs with h
  · exact le_refl 0
  · exact mul_nonneg hτ hW

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:111

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file