Documentation

Lean 4 Proof

theorem afterTaxReturn_decreasing {τ₁ τ₂ r : ℝ} (hr : 0 < r) (hτ : τ₁ < τ₂) :
    afterTaxReturn τ₂ r < afterTaxReturn τ₁ r := by
  simp only [afterTaxReturn]; nlinarith

Dependency Graph

Location

thesis/CESProofs/Macro/Accumulation.lean:182

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file