Documentation

Lean 4 Proof

theorem multiple_heirs_relax {r g : ℝ} {N : ℕ}
    (hg : -1 < g) (hN : 2 ≤ N) (hr : 1 + r < ↑N * (1 + g)) :
    wealthDilutionRatio r g N < 1 := by
  rw [self_correction_iff hg (by omega)]
  exact hr

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:263

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file