Documentation

Lean 4 Proof

theorem investmentRate_decreasing {s₀ ψ τ₁ τ₂ : ℝ}
    (hs : 0 < s₀) (hψ : 0 < ψ) (hτ : τ₁ < τ₂) :
    investmentRate s₀ ψ τ₂ < investmentRate s₀ ψ τ₁ := by
  simp only [investmentRate]
  have h1 : ψ * τ₁ < ψ * τ₂ := mul_lt_mul_of_pos_left hτ hψ
  have h2 : 1 - ψ * τ₂ < 1 - ψ * τ₁ := by linarith
  exact mul_lt_mul_of_pos_left h2 hs

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/GrowthTax.lean:128

Module Section

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

In the same file