Documentation

Lean 4 Proof

theorem npv_gap_increases_with_beta {η D₀ g₀ γ β₁ β₂ : ℝ}
    (hη : 0 < η) (hD : 0 < D₀) (hg : 0 < g₀)
    (hγ : 0 < γ) (_hβ₁ : 0 < β₁) (_hβ₂ : 0 < β₂)
    (hβ : β₁ < β₂) :
    npvOptimalBound η D₀ (γ + g₀ * β₁) < npvOptimalBound η D₀ (γ + g₀ * β₂) := by
  apply npv_gap_increases_with_delta hη hD
  · linarith [mul_pos hg _hβ₁]
  · linarith [mul_pos hg _hβ₂]
  · linarith [mul_lt_mul_of_pos_left hβ hg]

Dependency Graph

Location

thesis/CESProofs/Macro/GrowthTax.lean:394

Module Section

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

In the same file