Documentation

Lean 4 Proof

theorem discountGap_solow_still_dynamic {D₀ γ τ : ℝ} (hγ : 0 < γ)
    (hτ : 0 < τ) :
    D₀ < discountGap D₀ γ τ := by
  simp only [discountGap]
  linarith [mul_pos hγ hτ]

Dependency Graph

Location

thesis/CESProofs/Macro/GrowthTax.lean:183

Module Section

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

In the same file