Discount Gap

def proved Macroeconomics

Documentation

Lean 4 Proof

def discountGap (D₀ δ_gap τ : ℝ) : ℝ := D₀ + δ_gap * τ

Dependency Graph

Used by

discountGap_solow_still_dynamic dynamic_wedge_pos npvRevenue_cross_comparison discountGap_at_zero_tax dynamicWedge npv_suboptimal_at_laffer_peak discountGap_sensitivity higher_tax_wider_discount discountGap_increasing npv_no_dynamic_equals_static npvRevenue_decreasing_in_D npvRevenue npvRevenue_zero_rate npv_left_dominates_right npvRevenue_increasing_in_base discountGap_pos

Location

thesis/CESProofs/Macro/GrowthTax.lean:47

Module Section

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