Documentation

Lean 4 Proof

theorem tax_wedge_on_MPK {τ₁ τ₂ ρ_time δ : ℝ}
    (_hτ₁ : τ₁ < 1) (_hτ₂ : τ₂ < 1) :
    eulerSteadyStateMPK τ₂ ρ_time δ - eulerSteadyStateMPK τ₁ ρ_time δ =
    eulerSteadyStateReturn τ₂ ρ_time - eulerSteadyStateReturn τ₁ ρ_time := by
  simp only [eulerSteadyStateMPK, eulerSteadyStateReturn]; ring

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/Accumulation.lean:426

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file