Documentation

Lean 4 Proof

theorem lafferRevenue_increasing_below_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 : 2 * η * τ₂ ≤ 1 := 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:259

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file