Formalize sample-path Little's Law for deterministic continuous-time queueing trajectories, decomposed into area, sojourn, arrival-rate, boundary, and squeeze lemmas.
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
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.
No open leaves. Every sub-goal is proved or awaiting decomposition.