Documentation

Lean 4 Proof

theorem tax_revenue_feeds_debt {G R Y r_B g b : ℝ} (_hY : 0 < Y) :
    debtDynamics r_B g b (primaryDeficit G R Y) =
    (r_B - g) * b + (G - R) / Y := by
  simp only [debtDynamics, primaryDeficit]

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:470

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file