Documentation

Lean 4 Proof

theorem npv_gap_increases_with_delta {η D₀ δ₁ δ₂ : ℝ}
    (hη : 0 < η) (hD : 0 < D₀)
    (hδ₁ : 0 < δ₁) (hδ₂ : 0 < δ₂) (hδ : δ₁ < δ₂) :
    npvOptimalBound η D₀ δ₁ < npvOptimalBound η D₀ δ₂ := by
  simp only [npvOptimalBound]
  have hη_ne : η ≠ 0 := ne_of_gt hη
  have h2η : (0:ℝ) < 2 * η := by linarith
  have hden₁ : (0:ℝ) < D₀ + δ₁ / (2 * η) := by positivity
  have hden₂ : (0:ℝ) < D₀ + δ₂ / (2 * η) := by positivity
  have h8η2 : (0:ℝ) < 8 * η ^ 2 := by positivity
  rw [div_lt_div_iff₀ (mul_pos h8η2 hden₁) (mul_pos h8η2 hden₂)]
  have key₁ : 8 * η ^ 2 * (D₀ + δ₁ / (2 * η)) = 8 * η ^ 2 * D₀ + 4 * η * δ₁ := by
    field_simp; ring
  have key₂ : 8 * η ^ 2 * (D₀ + δ₂ / (2 * η)) = 8 * η ^ 2 * D₀ + 4 * η * δ₂ := by
    field_simp; ring
  have h_diff : δ₂ * (8 * η ^ 2 * (D₀ + δ₁ / (2 * η))) -
    δ₁ * (8 * η ^ 2 * (D₀ + δ₂ / (2 * η))) =
    8 * η ^ 2 * D₀ * (δ₂ - δ₁) := by
    rw [key₁, key₂]; ring
  linarith [mul_pos (mul_pos h8η2 hD) (sub_pos.mpr hδ)]

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/GrowthTax.lean:372

Module Section

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

In the same file