Documentation

Lean 4 Proof

theorem lafferRevenue_peak_is_max {B₀ η τ : ℝ}
    (hB : 0 < B₀) (hη : 0 < η) (_hτ_pos : 0 < τ) (_hτ_upper : τ < 1 / η)
    (hτ_ne : τ ≠ lafferPeak η) :
    lafferRevenue B₀ η τ < lafferRevenue B₀ η (lafferPeak η) := by
  by_cases h : τ < lafferPeak η
  · exact lafferRevenue_increasing_below_peak hB hη h (le_refl _)
  · push_neg at h
    have hlt : lafferPeak η < τ := lt_of_le_of_ne h (Ne.symm hτ_ne)
    exact lafferRevenue_decreasing_above_peak hB hη hlt (le_refl _)

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:289

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file