Documentation

Lean 4 Proof

theorem npv_solow_level_only {B₀ η D₀ τ : ℝ} :
    npvRevenue B₀ η D₀ 0 τ = lafferRevenue B₀ η τ / D₀ :=
  npv_no_dynamic_equals_static

Dependency Graph

Location

thesis/CESProofs/Macro/GrowthTax.lean:253

Module Section

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

In the same file