Documentation

Lean 4 Proof

theorem npvRevenue_decreasing_in_D {B₀ η D₀ δ₁ δ₂ τ : ℝ}
    (hR : 0 < lafferRevenue B₀ η τ)
    (hD₁ : 0 < discountGap D₀ δ₁ τ)
    (hδ : δ₁ < δ₂) (hτ : 0 < τ) :
    npvRevenue B₀ η D₀ δ₂ τ < npvRevenue B₀ η D₀ δ₁ τ := by
  simp only [npvRevenue]
  apply div_lt_div_of_pos_left hR hD₁
  simp only [discountGap]
  linarith [mul_lt_mul_of_pos_right hδ hτ]

Dependency Graph

Location

thesis/CESProofs/Macro/GrowthTax.lean:224

Module Section

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

In the same file