Documentation

Lean 4 Proof

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

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:276

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file