Documentation

Lean 4 Proof

theorem discountGap_sensitivity {γ g₀ β τ : ℝ} :
    discountGap (γ + g₀ * β) (γ + g₀ * β) τ =
    (γ + g₀ * β) * (1 + τ) := by
  simp only [discountGap]; ring

Dependency Graph

Location

thesis/CESProofs/Macro/GrowthTax.lean:176

Module Section

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

In the same file