Documentation

Lean 4 Proof

theorem npvOptimalBound_below_peak {η D₀ δ_gap : ℝ}
    (hη : 0 < η) (hD : 0 < D₀) (hδ : 0 < δ_gap) :
    npvOptimalBound η D₀ δ_gap < lafferPeak η := by
  simp only [npvOptimalBound, lafferPeak]
  have hη_ne : η ≠ 0 := ne_of_gt hη
  have h2η : (0:ℝ) < 2 * η := by linarith
  have hDstar : (0:ℝ) < D₀ + δ_gap / (2 * η) := by
    linarith [div_pos hδ h2η]
  have hden : (0:ℝ) < 8 * η ^ 2 * (D₀ + δ_gap / (2 * η)) := by positivity
  rw [div_lt_div_iff₀ hden h2η]
  have key : 8 * η ^ 2 * (D₀ + δ_gap / (2 * η)) =
      8 * η ^ 2 * D₀ + 4 * η * δ_gap := by field_simp; ring
  nlinarith [key, mul_pos hη hD, mul_pos hη hδ, sq_pos_of_pos hη]

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/GrowthTax.lean:316

Module Section

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

In the same file