NPV Optimal Bound

def proved Macroeconomics

Documentation

Lean 4 Proof

def npvOptimalBound (η D₀ δ_gap : ℝ) : ℝ :=
  δ_gap / (8 * η ^ 2 * (D₀ + δ_gap / (2 * η)))

Dependency Graph

Used by

npvOptimalBound_below_peak npv_gap_increases_with_delta npv_suboptimal_at_laffer_peak npv_gap_increases_with_beta npvOptimalBound_pos

Location

thesis/CESProofs/Macro/GrowthTax.lean:79

Module Section

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