Documentation

Lean 4 Proof

theorem eulerSteadyStateMPK_increasing_in_τ {τ₁ τ₂ ρ_time δ : ℝ}
    (hρ : 0 < ρ_time) (hτ₁ : τ₁ < 1) (hτ₂ : τ₂ < 1) (hτ : τ₁ < τ₂) :
    eulerSteadyStateMPK τ₁ ρ_time δ < eulerSteadyStateMPK τ₂ ρ_time δ := by
  simp only [eulerSteadyStateMPK]
  have h := eulerSteadyStateReturn_increasing_in_τ hρ hτ₁ hτ₂ hτ
  simp only [eulerSteadyStateReturn] at h
  linarith

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/Accumulation.lean:290

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file