queueing_general_littles_law

Proved

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

Consider a deterministic continuous-time queueing sample path with countably many jobs indexed by natural numbers in strict arrival order. Job n has arrival time arrival n, departure time departure n, and full sojourn time departure n - arrival n. Arrivals are locally finite, nonnegative, and strictly ordered; every job departs no earlier than it arrives. Departure order is arbitrary, so no FIFO assumption is made.

Let A(t) be the number of arrivals by time t, and let Q(t) be the number of jobs in system at time t, using the half-open convention arrival n ≤ t < departure n.

If the empirical arrival rate A(t) / t converges to lam as t tends to infinity, and the Cesaro average of full sojourn times of the first n jobs converges to Theta as n tends to infinity, then the time-average queue length converges to lam * Theta.

This current-environment root theorem is intended for the Prove2Me decomposition/project graph and imports Definitions.Def_queueing_continuous_time.

Formal statement

import Definitions.Def_queueing_continuous_time

open Filter
open scoped BigOperators Interval Topology
open QueueingLib.LittlesLaw.ContinuousTime

/--
General deterministic continuous-time Little's Law for simple arrivals.

Jobs are indexed in strict arrival order and may depart in arbitrary order.
If the empirical arrival rate converges to `lam` and the Cesaro mean of full
sojourn times converges to `Theta`, then the time-average number in system
converges to `lam * Theta`.

This theorem assumes simple arrivals (no simultaneous or batch arrivals), no
pre-time-zero jobs, and finite departure times for every indexed job. It makes
no probability, expectation, stationarity, ergodicity, or FIFO assumption.
-/
theorem queueing_general_littles_law
    (q : ContinuousSamplePath) (lam Theta : ℝ)
    (hArrivalRate : Tendsto (empiricalArrivalRate q) atTop (𝓝 lam))
    (hSojournMean : Tendsto (averageSojourn q) atTop (𝓝 Theta)) :
    Tendsto (timeAverageQueueLength q) atTop (𝓝 (lam * Theta)) := by
  sorry

Source

QueueingLib deterministic continuous-time Little's Law project. This current-environment root theorem is equivalent to the earlier submitted theorem general_littles_law (81236938-cf7e-49ad-a078-be9ba5432532), but imports the reusable queueing_continuous_time definition so it can share an environment with the submitted child theorem problems.

View graph