Documentation

Lean 4 Proof

theorem growthRate_pos {g₀ β τ : ℝ} (hg : 0 < g₀)
    (hbτ : β * τ < 1) :
    0 < growthRate g₀ β τ := by
  simp only [growthRate]
  exact mul_pos hg (by linarith)

Dependency Graph

Location

thesis/CESProofs/Macro/GrowthTax.lean:93

Module Section

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

In the same file