Documentation

Lean 4 Proof

theorem discountGap_pos {D₀ δ_gap τ : ℝ} (hD : 0 < D₀)
    (hδ : 0 ≤ δ_gap) (hτ : 0 ≤ τ) :
    0 < discountGap D₀ δ_gap τ := by
  simp only [discountGap]
  have : 0 ≤ δ_gap * τ := mul_nonneg hδ hτ
  linarith

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/GrowthTax.lean:153

Module Section

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

In the same file