Documentation

Lean 4 Proof

theorem dilution_ratio_pos {r g : ℝ} {N : ℕ}
    (hr : -1 < r) (hg : -1 < g) (hN : 0 < N) :
    0 < wealthDilutionRatio r g N := by
  simp only [wealthDilutionRatio]
  apply div_pos (by linarith)
  exact mul_pos (Nat.cast_pos.mpr hN) (by linarith)

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:226

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file