Documentation

Lean 4 Proof

theorem investmentRate_pos {s₀ ψ τ : ℝ} (hs : 0 < s₀)
    (hψτ : ψ * τ < 1) :
    0 < investmentRate s₀ ψ τ := by
  simp only [investmentRate]
  exact mul_pos hs (by linarith)

Dependency Graph

Location

thesis/CESProofs/Macro/GrowthTax.lean:121

Module Section

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

In the same file