Documentation

Lean 4 Proof

theorem tax_lowers_investment {s₀ ψ τ δ Y K : ℝ}
    (hs : 0 < s₀) (hψ : 0 < ψ) (hτ : 0 < τ)
    (hY : 0 < Y)
    (hss : capitalAccumulation (investmentRate s₀ ψ τ) δ Y K = 0) :
    capitalAccumulation (investmentRate s₀ ψ 0) δ Y K > 0 := by
  have hs_τ : investmentRate s₀ ψ τ < investmentRate s₀ ψ 0 :=
    investmentRate_decreasing hs hψ hτ
  have hss_eq := capitalAccumulation_eq_zero_iff.mp hss
  simp only [capitalAccumulation]
  nlinarith [mul_lt_mul_of_pos_right hs_τ hY]

Dependency Graph

Location

thesis/CESProofs/Macro/GrowthTax.lean:418

Module Section

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

In the same file