Documentation

Lean 4 Proof

theorem npvRevenue_cross_comparison {B₀ η D₀ δ_gap τ₁ τ₂ : ℝ}
    (hD₁ : 0 < discountGap D₀ δ_gap τ₁)
    (hD₂ : 0 < discountGap D₀ δ_gap τ₂)
    (hR₁D₂ : lafferRevenue B₀ η τ₁ * discountGap D₀ δ_gap τ₂ >
              lafferRevenue B₀ η τ₂ * discountGap D₀ δ_gap τ₁) :
    npvRevenue B₀ η D₀ δ_gap τ₂ < npvRevenue B₀ η D₀ δ_gap τ₁ := by
  simp only [npvRevenue]
  rw [div_lt_div_iff₀ hD₂ hD₁]
  linarith

Dependency Graph

Location

thesis/CESProofs/Macro/GrowthTax.lean:235

Module Section

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

In the same file