Documentation

Lean 4 Proof

theorem levelEffect_links_solow {s₀ ψ δ τ : ℝ} :
    levelEffect s₀ ψ δ τ = steadyStateKY (investmentRate s₀ ψ τ) δ := by
  simp only [levelEffect, steadyStateKY]

Dependency Graph

Location

thesis/CESProofs/Macro/GrowthTax.lean:144

Module Section

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

In the same file