Documentation

Lean 4 Proof

theorem lafferRevenue_decreasing_above_peak {B₀ η τ₁ τ₂ : ℝ}
    (hB : 0 < B₀) (hη : 0 < η) (hτ : τ₁ < τ₂)
    (hτ₁ : lafferPeak η ≤ τ₁) :
    lafferRevenue B₀ η τ₂ < lafferRevenue B₀ η τ₁ := by
  simp only [lafferRevenue, lafferPeak] at *
  have key : τ₁ * B₀ * (1 - η * τ₁) - τ₂ * B₀ * (1 - η * τ₂) =
      B₀ * (τ₂ - τ₁) * (η * (τ₁ + τ₂) - 1) := by ring
  have h2η : (0:ℝ) < 2 * η := by linarith
  have h_clear : 1 ≤ 2 * η * τ₁ := by
    have h := mul_le_mul_of_nonneg_left hτ₁ (le_of_lt h2η)
    rw [mul_one_div_cancel (ne_of_gt h2η)] at h; linarith
  have hf : 0 < η * (τ₁ + τ₂) - 1 := by nlinarith
  linarith [mul_pos (mul_pos hB (show (0:ℝ) < τ₂ - τ₁ by linarith)) hf]

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/TaxStructure.lean:274

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file