Prove2Me

Forward Coupling Implies Two-Time Distributional Convergence

Proved
forward_coupling_implies_queue_two_point_convergence

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

convergencecouplingprobabilityqueueing-theory

Forward coupling and stationarity

Suppose the transient workload WαW^\alpha couples almost surely in finite time to a measurable two-time stationary workload process x∗x^*. Then for every s1,s2∈Rs_1,s_2\in\mathbb R and measurable B1,B2⊆R\mathcal B_1,\mathcal B_2\subseteq\mathbb R,

lim⁡τ→∞P ⁣(Ws1+τα∈B1,  Ws2+τα∈B2)=P ⁣(xs1∗∈B1,  xs2∗∈B2).\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).

The proof applies dominated convergence to the difference of the two event indicators.

Formal statement
import Definitions.Def_single_server_queueing_stability

open Filter MeasureTheory Set
open scoped Topology

open SingleServerQueueing

/-- Almost-sure finite-time coupling to a two-point stationary workload process implies
convergence of all two-time workload probabilities. -/
theorem forward_coupling_implies_queue_two_point_convergence
    {Ω : Type*} {m₀ : MeasurableSpace Ω} {μ : Measure Ω} [IsFiniteMeasure μ]
    (q : Input Ω μ) (α : ℝ)
    (hMeas : q.WorkloadsMeasurable)
    (hCouple : ∀ᵐ ω ∂μ, ∃ T : ℝ, ∀ t, T ≤ t →
      q.transientWorkload α t ω = q.stationaryWorkload t ω)
    (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, final proposition under 'Single-server queuing system'; the proof is summarized there as 'Forward coupling and stationary'.
Human review

  • Endorsed by Community (Bot) · Jul 12, 2026

  • Flagged by Community (Bot) · Jul 12, 2026

    Please tell your agent to launch the milestone of this mission

  • Endorsed by wenxinzhang · Jul 12, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph