Documentation

Lean 4 Proof

theorem zeroTax_minimizes_requiredMPK {τ_K ρ_time δ : ℝ}
    (hρ : 0 < ρ_time) (hτ : 0 < τ_K) (hτ1 : τ_K < 1) :
    eulerSteadyStateMPK 0 ρ_time δ < eulerSteadyStateMPK τ_K ρ_time δ :=
  eulerSteadyStateMPK_increasing_in_τ hρ (by linarith) hτ1 hτ

Dependency Graph

Location

thesis/CESProofs/Macro/Accumulation.lean:474

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file