Documentation

Lean 4 Proof

theorem npv_suboptimal_at_laffer_peak {B₀ η D₀ δ_gap : ℝ}
    (hB : 0 < B₀) (hη : 0 < η)
    (hD : 0 < D₀) (hδ : 0 < δ_gap) :
    ∃ τ₁ : ℝ, τ₁ < lafferPeak η ∧
      npvRevenue B₀ η D₀ δ_gap (lafferPeak η) <
      npvRevenue B₀ η D₀ δ_gap τ₁ := by
  use lafferPeak η - npvOptimalBound η D₀ δ_gap
  have hε_pos := npvOptimalBound_pos hη hD hδ
  have hε_small := npvOptimalBound_below_peak hη hD hδ
  refine ⟨by linarith, ?_⟩
  -- Show NPV(τ*) < NPV(τ₁) via cross-multiplication
  simp only [npvRevenue]
  have hη_ne : η ≠ 0 := ne_of_gt hη
  have h2η_pos : (0:ℝ) < 2 * η := by linarith
  have hDstar_pos : (0:ℝ) < D₀ + δ_gap / (2 * η) := by positivity
  have h8η2D_pos : (0:ℝ) < 8 * η ^ 2 * (D₀ + δ_gap / (2 * η)) := by positivity
  -- Positivity of discount gaps
  have hD₁ : 0 < discountGap D₀ δ_gap (lafferPeak η - npvOptimalBound η D₀ δ_gap) := by
    apply discountGap_pos hD (le_of_lt hδ)
    linarith [lafferPeak_pos hη]
  have hD_star : 0 < discountGap D₀ δ_gap (lafferPeak η) := by
    apply discountGap_pos hD (le_of_lt hδ)
    exact le_of_lt (lafferPeak_pos hη)
  rw [div_lt_div_iff₀ hD_star hD₁]
  -- Goal: R(τ*) · D(τ₁) < R(τ₁) · D(τ*)
  -- Unfold everything to rational expressions
  simp only [lafferRevenue, lafferPeak, discountGap, npvOptimalBound]
  -- Clear all denominators
  field_simp
  -- Close the polynomial inequality
  nlinarith [sq_nonneg η, sq_nonneg D₀, sq_nonneg δ_gap, sq_nonneg B₀,
             mul_pos hB hδ, mul_pos hη hD, mul_pos hη hδ, sq_pos_of_pos hη]

Dependency Graph

Location

thesis/CESProofs/Macro/GrowthTax.lean:338

Module Section

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

In the same file