Documentation

Lean 4 Proof

theorem npv_no_dynamic_equals_static {B₀ η D₀ τ : ℝ} :
    npvRevenue B₀ η D₀ 0 τ = lafferRevenue B₀ η τ / D₀ := by
  simp only [npvRevenue, discountGap]; ring

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/GrowthTax.lean:247

Module Section

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

In the same file