Documentation

Lean 4 Proof

theorem npvOptimalBound_pos {η D₀ δ_gap : ℝ}
    (hη : 0 < η) (hD : 0 < D₀) (hδ : 0 < δ_gap) :
    0 < npvOptimalBound η D₀ δ_gap := by
  simp only [npvOptimalBound]
  apply div_pos hδ
  apply mul_pos (by positivity : (0:ℝ) < 8 * η ^ 2)
  linarith [div_pos hδ (show (0:ℝ) < 2 * η by linarith)]

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/GrowthTax.lean:306

Module Section

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

In the same file