Sections / Section 14: Macro -- Two-Factor CES, Growth, Tax / debtDynamics

Debt Dynamics

defprovedMacroeconomics

Documentation

Lean 4 Proof

def debtDynamics (r_B g b d : ℝ) : ℝ := (r_B - g) * b + d

Dependency Graph

Used by

debtSustainable_zero_debt debtSustainable debtDynamics_increasing_in_r debt_sustainable_with_growth taxRevenue_feeds_debt tax_revenue_feeds_debt debtDynamics_eq_zero_iff debtSustainable_iff debtDynamics_decreasing_in_g

Location

thesis/CESProofs/Macro/TaxStructure.lean:93

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file

taxRevenue taxRevenueShare corporateProfit profitShare lafferRevenue lafferPeak lafferMaxRevenue saezTopRate primaryDeficit debtSustainable taxRevenue_zero_rates taxRevenue_scale taxRevenue_additive taxRevenue_increasing_in_τL taxRevenue_increasing_in_τK taxRevenue_increasing_in_τC taxRevenue_increasing_in_τcorp corporateProfit_pos corporateProfit_increasing_in_Y corporateProfit_decreasing_in_Jσ