Documentation

Lean 4 Proof

theorem debt_sustainable_with_growth {r_B g₁ g₂ b d : ℝ}
    (hb : 0 < b) (hg : g₁ < g₂) :
    debtDynamics r_B g₂ b d < debtDynamics r_B g₁ b d :=
  debtDynamics_decreasing_in_g hb hg

Dependency Graph

Location

thesis/CESProofs/Macro/GrowthTax.lean:436

Module Section

Growth and Dynamic Tax Revenue (Layer 4-5 of Macro Extension)

In the same file