general_littles_law

import Mathlib

/-!
# General deterministic continuous-time Little's Law

This file states a continuous-time, non-FIFO sample-path theorem for jobs indexed
in strict arrival order. It contains no probability, expectation, stationarity,
or ergodicity assumptions.
-/

namespace QueueingLib.LittlesLaw.ContinuousTime

open Filter
open scoped BigOperators Interval Topology

/--
A locally finite continuous-time queueing sample path with simple arrivals.

Jobs are indexed by `Nat` in strict arrival order. The finite set `arrivedBy t`
contains exactly the jobs whose arrival epoch is at most `t`. Requiring these
sets to be finite encodes local finiteness of arrivals. Departures need not occur
in arrival order, so this model does not impose FIFO.

The field `strictMono_arrival` excludes simultaneous or batch arrivals. The
field `arrival_nonneg` excludes jobs present before time zero while permitting
jobs to arrive at time zero. Since departure epochs are real numbers, every
indexed job has a finite departure time.
-/
structure ContinuousSamplePath where
  arrival : Nat → ℝ
  departure : Nat → ℝ
  arrivedBy : ℝ → Finset Nat
  mem_arrivedBy : ∀ t n, n ∈ arrivedBy t ↔ arrival n ≤ t
  arrival_nonneg : ∀ n, 0 ≤ arrival n
  strictMono_arrival : StrictMono arrival
  arrival_le_departure : ∀ n, arrival n ≤ departure n

/-- Jobs that have departed by time `t`, regardless of departure order. -/
noncomputable def departedBy (q : ContinuousSamplePath) (t : ℝ) : Finset Nat :=
  (q.arrivedBy t).filter fun n => q.departure n ≤ t

/-- `A(t)`, the number of arrivals by time `t`. -/
def arrivalCount (q : ContinuousSamplePath) (t : ℝ) : Nat :=
  (q.arrivedBy t).card

/-- `D(t)`, the number of departures by time `t`. -/
noncomputable def departureCount (q : ContinuousSamplePath) (t : ℝ) : Nat :=
  (departedBy q t).card

/--
`Q(t)`, the number of active jobs at time `t`. A job is active on the half-open
interval from its arrival epoch through, but not including, its departure epoch.
-/
noncomputable def queueLength (q : ContinuousSamplePath) (t : ℝ) : Nat :=
  ((q.arrivedBy t).filter fun n => t < q.departure n).card

/-- `theta n`, the full sojourn time of job `n`. -/
def sojournTime (q : ContinuousSamplePath) (n : Nat) : ℝ :=
  q.departure n - q.arrival n

/-- Sum of the sojourn times of jobs `0, ..., n - 1`, using zero-based indexing. -/
def cumulativeSojourn (q : ContinuousSamplePath) (n : Nat) : ℝ :=
  ∑ i ∈ Finset.range n, sojournTime q i

/-- Average sojourn time of the first `n` jobs. The value at `n = 0` is zero. -/
noncomputable def averageSojourn (q : ContinuousSamplePath) (n : Nat) : ℝ :=
  cumulativeSojourn q n / (n : ℝ)

/-- Empirical arrival rate `A(t) / t`. -/
noncomputable def empiricalArrivalRate (q : ContinuousSamplePath) (t : ℝ) : ℝ :=
  (arrivalCount q t : ℝ) / t

/-- The continuous-time average queue length over `[0, t]`. -/
noncomputable def timeAverageQueueLength (q : ContinuousSamplePath) (t : ℝ) : ℝ :=
  (∫ s in (0 : ℝ)..t, (queueLength q s : ℝ)) / t

/-- Total sojourn of jobs departed by `t`, normalized by `t`. -/
noncomputable def departedSojournRate (q : ContinuousSamplePath) (t : ℝ) : ℝ :=
  (∑ n ∈ departedBy q t, sojournTime q n) / t

/-- Total sojourn of jobs arrived by `t`, normalized by `t`. -/
noncomputable def arrivedSojournRate (q : ContinuousSamplePath) (t : ℝ) : ℝ :=
  (∑ n ∈ q.arrivedBy t, sojournTime q n) / t

/-- Total sojourn of jobs at least `N` that arrived by `t`. -/
noncomputable def arrivedTailSojourn
    (q : ContinuousSamplePath) (N : Nat) (t : ℝ) : ℝ :=
  ∑ n ∈ (q.arrivedBy t).filter (fun n => N ≤ n), sojournTime q n

/--
The tail arrived-sojourn total at the earlier time `t / (1 + eps)`, normalized
by the original horizon `t`.
-/
noncomputable def scaledArrivedTailSojournRate
    (q : ContinuousSamplePath) (N : Nat) (eps t : ℝ) : ℝ :=
  arrivedTailSojourn q N (t / (1 + eps)) / t

end QueueingLib.LittlesLaw.ContinuousTime

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 Cesàro 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 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