Documentation

Lean 4 Proof

theorem lafferRevenue_at_peak {B₀ η : ℝ} (hη : η ≠ 0) :
    lafferRevenue B₀ η (lafferPeak η) = lafferMaxRevenue B₀ η := by
  simp only [lafferRevenue, lafferPeak, lafferMaxRevenue]; field_simp; ring

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:216

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file