Documentation

Lean 4 Proof

theorem growthRate_decreasing {g₀ β τ₁ τ₂ : ℝ}
    (hg : 0 < g₀) (hβ : 0 < β) (hτ : τ₁ < τ₂) :
    growthRate g₀ β τ₂ < growthRate g₀ β τ₁ := by
  simp only [growthRate]
  have h1 : β * τ₁ < β * τ₂ := mul_lt_mul_of_pos_left hτ hβ
  have h2 : 1 - β * τ₂ < 1 - β * τ₁ := by linarith
  exact mul_lt_mul_of_pos_left h2 hg

Dependency Graph

Location

thesis/CESProofs/Macro/GrowthTax.lean:107

Module Section

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

In the same file