Higher Tax Higher Required Return

theorem proved Macroeconomics

Documentation

Lean 4 Proof

theorem higherTax_higherRequiredReturn {τ₁ τ₂ ρ_time δ : ℝ}
    (hρ : 0 < ρ_time) (hτ₁ : τ₁ < 1) (hτ₂ : τ₂ < 1) (hτ : τ₁ < τ₂) :
    eulerSteadyStateMPK τ₁ ρ_time δ < eulerSteadyStateMPK τ₂ ρ_time δ :=
  eulerSteadyStateMPK_increasing_in_τ hρ hτ₁ hτ₂ hτ

Dependency Graph

Location

thesis/CESProofs/Macro/Accumulation.lean:450

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)