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

Discount Gap At Zero Tax

theoremprovedMacroeconomics

Documentation

Lean 4 Proof

theorem discountGap_at_zero_tax {D₀ δ_gap : ℝ} :
    discountGap D₀ δ_gap 0 = D₀ := by
  simp only [discountGap]; ring

Dependency Graph

Location

thesis/CESProofs/Macro/GrowthTax.lean:161

Module Section

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

In the same file

growthRate investmentRate discountGap npvRevenue levelEffect growthDrag dynamicWedge npvOptimalBound balancedGrowthOutput growthRate_pos growthRate_at_zero_tax growthRate_decreasing growthRate_solow_constant investmentRate_pos investmentRate_decreasing levelEffect_decreasing levelEffect_links_solow discountGap_pos discountGap_increasing discountGap_sensitivity