Documentation

Lean 4 Proof

theorem npvRevenue_increasing_in_base {B₀₁ B₀₂ η D₀ δ_gap τ : ℝ}
    (hD : 0 < discountGap D₀ δ_gap τ)
    (hτ : 0 < τ) (hτu : η * τ < 1) (hB : B₀₁ < B₀₂) :
    npvRevenue B₀₁ η D₀ δ_gap τ < npvRevenue B₀₂ η D₀ δ_gap τ := by
  simp only [npvRevenue]
  apply div_lt_div_of_pos_right _ hD
  simp only [lafferRevenue]
  have h1 : 0 < 1 - η * τ := by linarith
  have h2 : 0 < τ * (1 - η * τ) := mul_pos hτ h1
  nlinarith [mul_lt_mul_of_pos_right hB h2]

Dependency Graph

Location

thesis/CESProofs/Macro/GrowthTax.lean:212

Module Section

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

In the same file