Documentation

Lean 4 Proof

theorem higher_tax_wider_discount {D₀ δ_gap τ₁ τ₂ : ℝ}
    (hδ : 0 < δ_gap) (hτ : τ₁ < τ₂) :
    discountGap D₀ δ_gap τ₁ < discountGap D₀ δ_gap τ₂ :=
  discountGap_increasing hδ hτ

Dependency Graph

Location

thesis/CESProofs/Macro/GrowthTax.lean:430

Module Section

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

In the same file