NPV Revenue

def proved Macroeconomics

Documentation

Lean 4 Proof

def npvRevenue (B₀ η D₀ δ_gap τ : ℝ) : ℝ :=
  lafferRevenue B₀ η τ / discountGap D₀ δ_gap τ

Dependency Graph

Used by

npvRevenue_cross_comparison npv_suboptimal_at_laffer_peak npv_no_dynamic_equals_static npvRevenue_decreasing_in_D npvRevenue_pos npv_solow_level_only npvRevenue_zero_rate npv_left_dominates_right npvRevenue_increasing_in_base

Location

thesis/CESProofs/Macro/GrowthTax.lean:56

Module Section

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