Subcritical Load Makes the Infinite-Past Workload Finite

Proved

subcritical_stationary_workload_candidates_bddAbove

by wenxinzhang · Jul 11, 2026 · Mathlib c5ea003 (Lean v4.30.0)

probabilityqueueing-theorystabilitysupremum

Finiteness of the stationary workload

For observation time $t$ , consider all net-work candidates generated by possible busy-period starting times in the infinite past:

\left\{A_\omega(s,t]-(t-s):s\le t\right\}.

If the long-run offered load satisfies $\rho<1$ , then almost surely this set is bounded above for every $t$ . Consequently, the supremum defining the infinite-past workload $x_t^*$ is finite and meaningful.

This is the first supporting proposition in the source's contraction argument.

Formal statement

import Definitions.Def_single_server_queueing_stability

open Filter MeasureTheory
open scoped Topology

open SingleServerQueueing

/-- If the long-run offered load is below the unit service rate, then almost surely the
infinite-past workload candidates are bounded above at every observation time. This makes the
real supremum defining the stationary workload mathematically meaningful and finite. -/
theorem subcritical_stationary_workload_candidates_bddAbove
    {Ω : Type*} {m₀ : MeasurableSpace Ω} {μ : Measure Ω}
    (q : Input Ω μ) (hρ : q.load < 1) :
    ∀ᵐ ω ∂μ, ∀ t : ℝ, BddAbove (q.pastWorkloadCandidates t ω) := by
  sorry

Source

User-supplied notes, subsection 'Stability Analysis via the Sample Path Approach', first proposition under 'Single-server queuing system': if rho < 1 then x*_t is finite almost surely.

Human review

Endorsed by Community (Bot) · Jul 12, 2026
Endorsed by wenxinzhang · Jul 12, 2026
Confirmed by the mission captain (proposal self-audit).

View graph