Documentation

Lean 4 Proof

theorem lafferRevenue_symmetric {B₀ η ε : ℝ} (hη : η ≠ 0) :
    lafferRevenue B₀ η (lafferPeak η - ε) =
    lafferRevenue B₀ η (lafferPeak η + ε) := by
  simp only [lafferRevenue, lafferPeak]
  field_simp
  ring

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/GrowthTax.lean:264

Module Section

Growth and Dynamic Tax Revenue (Layer 4-5 of Macro Extension)

In the same file