Documentation

Lean 4 Proof

theorem npv_left_dominates_right {B₀ η D₀ δ_gap ε : ℝ}
    (hB : 0 < B₀) (hη : 0 < η)
    (hε : 0 < ε) (hε_small : ε < lafferPeak η)
    (hD : 0 < D₀) (hδ_nn : 0 ≤ δ_gap) (hδ : 0 < δ_gap) :
    npvRevenue B₀ η D₀ δ_gap (lafferPeak η + ε) <
    npvRevenue B₀ η D₀ δ_gap (lafferPeak η - ε) := by
  simp only [npvRevenue]
  rw [← lafferRevenue_symmetric (ne_of_gt hη)]
  have hR : 0 < lafferRevenue B₀ η (lafferPeak η - ε) :=
    lafferRevenue_pos_near_peak hB hη hε hε_small
  have hD₁ : 0 < discountGap D₀ δ_gap (lafferPeak η - ε) := by
    apply discountGap_pos hD hδ_nn
    linarith [lafferPeak_pos hη]
  exact div_lt_div_of_pos_left hR hD₁
    (discountGap_increasing hδ (by linarith))

Dependency Graph

Location

thesis/CESProofs/Macro/GrowthTax.lean:289

Module Section

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

In the same file