Documentation

Lean 4 Proof

theorem npvRevenue_pos {B₀ η D₀ δ_gap τ : ℝ}
    (hB : 0 < B₀) (_hη : 0 < η) (hτ : 0 < τ) (hτu : η * τ < 1)
    (hD : 0 < D₀) (hδ : 0 ≤ δ_gap) :
    0 < npvRevenue B₀ η D₀ δ_gap τ := by
  simp only [npvRevenue]
  have hR : 0 < lafferRevenue B₀ η τ := by
    simp only [lafferRevenue]
    have h1 : 0 < 1 - η * τ := by linarith
    have h2 : 0 < τ * B₀ := mul_pos hτ hB
    nlinarith [mul_pos h2 h1]
  exact div_pos hR (discountGap_pos hD hδ (le_of_lt hτ))

Dependency Graph

Location

thesis/CESProofs/Macro/GrowthTax.lean:194

Module Section

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

In the same file