Documentation

Lean 4 Proof

theorem self_correction_iff {r g : ℝ} {N : ℕ}
    (hg : -1 < g) (hN : 0 < N) :
    wealthDilutionRatio r g N < 1 ↔ 1 + r < ↑N * (1 + g) := by
  simp only [wealthDilutionRatio]
  rw [div_lt_one (mul_pos (Nat.cast_pos.mpr hN) (by linarith))]

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:242

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file