Single-Server Queueing Convergence Under $\rho<1$

Proved

single_server_queueing_convergence_of_subcritical

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

convergencecouplingprobabilityqueueing-theorystabilitystochastic-processes

Single-server queueing convergence under subcritical load

Let $A_\omega(s,t]$ be the cumulative service work arriving to a continuous-time, infinite-buffer single-server queue during $(s,t]$ . The server works at unit rate. Let $W_t^\alpha$ be the reflected workload process initialized with finite workload $\alpha\ge0$ , and let $x_t^*$ be the infinite-past workload.

Assume that the long-run offered load is below capacity, $\rho<1$ , that the workload observables are measurable, and that $x^*$ is stationary in its two-time finite-dimensional distributions. Then, for every $s_1,s_2\in\mathbb R$ and measurable sets $\mathcal B_1,\mathcal B_2\subseteq\mathbb R$ ,

\lim_{\tau\to\infty}\mathbb P\!\left(W_{s_1+\tau}^\alpha\in\mathcal B_1,\;W_{s_2+\tau}^\alpha\in\mathcal B_2\right)=\mathbb P\!\left(x_{s_1}^*\in\mathcal B_1,\;x_{s_2}^*\in\mathcal B_2\right).

Thus the transient workload converges in its two-time finite-dimensional distributions to the stationary workload. The proof factors through finite-time coupling under $\rho<1$ and then dominated convergence.

Formal statement

import Definitions.Def_single_server_queueing_stability

open Filter MeasureTheory Set
open scoped Topology

open SingleServerQueueing

/-- **Single-server queueing convergence under subcritical load.** For a stationary queueing
input whose offered load is below the unit service rate, the workload from every finite
nonnegative initial condition converges in its two-time finite-dimensional distributions to the
stationary workload constructed from the infinite past. -/
theorem single_server_queueing_convergence_of_subcritical
    {Ω : Type*} {m₀ : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ]
    (q : Input Ω μ) (α : ℝ) (hα : 0 ≤ α)
    (hρ : q.load < 1) (hMeas : q.WorkloadsMeasurable)
    (hStationary : IsTwoPointStationary μ q.stationaryWorkload)
    (s₁ s₂ : ℝ) (B₁ B₂ : Set ℝ) (hB₁ : MeasurableSet B₁) (hB₂ : MeasurableSet B₂) :
    Tendsto
      (fun τ ↦ μ.real {ω | q.transientWorkload α (s₁ + τ) ω ∈ B₁ ∧
        q.transientWorkload α (s₂ + τ) ω ∈ B₂})
      atTop
      (nhds (μ.real {ω | q.stationaryWorkload s₁ ω ∈ B₁ ∧
        q.stationaryWorkload s₂ ω ∈ B₂})) := by
  sorry

Source

User-supplied notes, subsection 'Stability Analysis via the Sample Path Approach', final proposition under 'Single-server queuing system'. The preceding proposition proves finite-time coupling under load rho < 1; stationarity plus forward coupling yields the stated convergence. Apparent source typos on the right-hand side, x*_{s_s} and B_s, are interpreted as x*_{s2} and B2.

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

Single-Server Queueing Convergence Under ρ<1\rho<1ρ<1

Single-server queueing convergence under subcritical load

Single-Server Queueing Convergence Under $\rho<1$