Documentation

Lean 4 Proof

theorem discountGap_increasing {D₀ δ_gap τ₁ τ₂ : ℝ}
    (hδ : 0 < δ_gap) (hτ : τ₁ < τ₂) :
    discountGap D₀ δ_gap τ₁ < discountGap D₀ δ_gap τ₂ := by
  simp only [discountGap]
  linarith [mul_lt_mul_of_pos_left hτ hδ]

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/GrowthTax.lean:166

Module Section

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

In the same file