Documentation

Lean 4 Proof

theorem lafferRevenue_strictly_concave {B₀ η τ₁ τ₂ : ℝ}
    (hB : 0 < B₀) (hη : 0 < η) (hτ : τ₁ < τ₂) :
    (lafferRevenue B₀ η τ₁ + lafferRevenue B₀ η τ₂) / 2 <
    lafferRevenue B₀ η ((τ₁ + τ₂) / 2) := by
  simp only [lafferRevenue]
  have key : (τ₁ + τ₂) / 2 * B₀ * (1 - η * ((τ₁ + τ₂) / 2)) -
      (τ₁ * B₀ * (1 - η * τ₁) + τ₂ * B₀ * (1 - η * τ₂)) / 2 =
      B₀ * η * (τ₂ - τ₁) ^ 2 / 4 := by ring
  have h_sq : 0 < (τ₂ - τ₁) ^ 2 := sq_pos_of_pos (by linarith)
  nlinarith [mul_pos (mul_pos hB hη) h_sq]

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:245

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file