Documentation

Lean 4 Proof

theorem npvRevenue_zero_rate {B₀ η D₀ δ_gap : ℝ} :
    npvRevenue B₀ η D₀ δ_gap 0 = 0 := by
  simp only [npvRevenue, lafferRevenue, discountGap]; ring

Dependency Graph

Location

thesis/CESProofs/Macro/GrowthTax.lean:207

Module Section

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

In the same file