Documentation

Lean 4 Proof

theorem debtDynamics_decreasing_in_g {r_B g₁ g₂ b d : ℝ}
    (hb : 0 < b) (hg : g₁ < g₂) :
    debtDynamics r_B g₂ b d < debtDynamics r_B g₁ b d := by
  simp only [debtDynamics]; nlinarith

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/TaxStructure.lean:384

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file