Documentation

Lean 4 Proof

theorem eulerSteadyStateMPK_eq {τ_K ρ_time δ : ℝ} :
    eulerSteadyStateMPK τ_K ρ_time δ =
    eulerSteadyStateReturn τ_K ρ_time + δ := by
  simp only [eulerSteadyStateMPK, eulerSteadyStateReturn]

Dependency Graph

Location

thesis/CESProofs/Macro/Accumulation.lean:261

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file