Documentation

Lean 4 Proof

theorem lafferRevenue_pos_near_peak {B₀ η ε : ℝ}
    (hB : 0 < B₀) (hη : 0 < η) (hε : 0 < ε) (hε_small : ε < lafferPeak η) :
    0 < lafferRevenue B₀ η (lafferPeak η - ε) := by
  have hτ_pos : 0 < lafferPeak η - ε := by
    have := lafferPeak_pos hη; linarith
  simp only [lafferRevenue, lafferPeak]
  have hη_ne : η ≠ 0 := ne_of_gt hη
  have h_factor : 1 - η * (1 / (2 * η) - ε) = 1 / 2 + η * ε := by field_simp; ring
  rw [h_factor]
  have h1 : 0 < 1 / 2 + η * ε := by positivity
  have h2 : 0 < 1 / (2 * η) - ε := by
    simp only [lafferPeak] at hε_small; linarith
  positivity

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/GrowthTax.lean:273

Module Section

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

In the same file