Debt Dynamics Increasing In R

theorem proved Macroeconomics

Documentation

Lean 4 Proof

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

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:391

Module Section

Government Tax Structure (Layer 3 of Macro Extension)