def balancedGrowthOutput (Y₀ g : ℝ) (t : ℕ) : ℝ := Y₀ * (1 + g) ^ t
thesis/CESProofs/Macro/GrowthTax.lean:85
Growth and Dynamic Tax Revenue (Layer 4-5 of Macro Extension)