Documentation

Lean 4 Proof

theorem levelEffect_decreasing {s₀ ψ δ τ₁ τ₂ : ℝ}
    (hs : 0 < s₀) (hψ : 0 < ψ) (hδ : 0 < δ) (hτ : τ₁ < τ₂) :
    levelEffect s₀ ψ δ τ₂ < levelEffect s₀ ψ δ τ₁ := by
  simp only [levelEffect]
  exact div_lt_div_of_pos_right (investmentRate_decreasing hs hψ hτ) hδ

Dependency Graph

Location

thesis/CESProofs/Macro/GrowthTax.lean:137

Module Section

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

In the same file