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

Saez Top Rate

defprovedMacroeconomics

Documentation

Lean 4 Proof

def saezTopRate (a e : ℝ) : ℝ := 1 / (1 + a * e)

Dependency Graph

Used by

saezTopRate_zero_elasticity saezTopRate_pos saezTopRate_specialization saezTopRate_lt_one ramsey_inverse_elasticity saezTopRate_decreasing_in_e saezTopRate_decreasing_in_a saezTopRate_us_calibration

Location

thesis/CESProofs/Macro/TaxStructure.lean:78

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file

taxRevenue taxRevenueShare corporateProfit profitShare lafferRevenue lafferPeak lafferMaxRevenue 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σ