Subcritical Single-Server Workloads Couple in Finite Time

Proved

subcritical_single_server_queue_eventually_couples

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

couplingprobabilityqueueing-theorystability

Finite-time coupling under subcritical load

Consider the unit-rate single-server queue defined by the cumulative work input $A_\omega(s,t]$ . Let $W_t^\alpha$ be the workload initialized with finite $\alpha \ge 0$ , and let $x_t^*$ be the workload constructed from the infinite past.

If the long-run offered load satisfies $\rho<1$ , then almost surely there is a finite random time $T$ such that

W_t^\alpha=x_t^* \qquad \text{for every }t\ge T.

This is the sample-path contraction proposition in the source notes.

Formal statement

import Definitions.Def_single_server_queueing_stability

open Filter MeasureTheory
open scoped Topology

open SingleServerQueueing

/-- In a unit-rate single-server queue with long-run offered load below one, every workload
started from finite nonnegative work couples after an almost surely finite time to the workload
constructed from the infinite past. -/
theorem subcritical_single_server_queue_eventually_couples
    {Ω : Type*} {m₀ : MeasurableSpace Ω} {μ : Measure Ω}
    (q : Input Ω μ) (α : ℝ) (hα : 0 ≤ α) (hρ : q.load < 1) :
    ∀ᵐ ω ∂μ, ∃ T : ℝ, ∀ t, T ≤ t →
      q.transientWorkload α t ω = q.stationaryWorkload t ω := by
  sorry

Source

User-supplied notes, subsection 'Stability Analysis via the Sample Path Approach', penultimate proposition: if rho < 1 then the coupling time T^alpha 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