Documentation

Lean 4 Proof

theorem tax_wedge_pos {τ₁ τ₂ ρ_time δ : ℝ}
    (hρ : 0 < ρ_time) (hτ₁ : τ₁ < 1) (hτ₂ : τ₂ < 1) (hτ : τ₁ < τ₂) :
    0 < eulerSteadyStateMPK τ₂ ρ_time δ - eulerSteadyStateMPK τ₁ ρ_time δ := by
  rw [tax_wedge_on_MPK hτ₁ hτ₂]
  linarith [eulerSteadyStateReturn_increasing_in_τ hρ hτ₁ hτ₂ hτ]

Dependency Graph

Location

thesis/CESProofs/Macro/Accumulation.lean:433

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file