Documentation

Lean 4 Proof

theorem single_heir_piketty {r g : ℝ} (hg : -1 < g) :
    wealthDilutionRatio r g 1 < 1 ↔ r < g := by
  rw [self_correction_iff hg (by norm_num : 0 < 1)]
  simp [Nat.cast_one]

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:253

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file