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

Laffer Revenue

defprovedMacroeconomics

Documentation

Lean 4 Proof

def lafferRevenue (B₀ η τ : ℝ) : ℝ := τ * B₀ * (1 - η * τ)

Dependency Graph

Used by

dynamic_wedge_pos lafferRevenue_peak_is_max npvRevenue_cross_comparison dynamicWedge lafferRevenue_at_peak npv_suboptimal_at_laffer_peak lafferRevenue_zero_rate npv_no_dynamic_equals_static lafferRevenue_increasing_below_peak lafferRevenue_strictly_concave npvRevenue_decreasing_in_D npvRevenue_pos npvRevenue npv_solow_level_only npvRevenue_zero_rate lafferRevenue_decreasing_above_peak lafferRevenue_symmetric npv_left_dominates_right npvRevenue_increasing_in_base lafferRevenue_zero_at_upper lafferRevenue_pos_near_peak

Location

thesis/CESProofs/Macro/TaxStructure.lean:64

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file

taxRevenue taxRevenueShare corporateProfit profitShare lafferPeak lafferMaxRevenue saezTopRate primaryDeficit debtDynamics 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σ