arrivedSojournRate_tendsto

import Definitions.Def_queueing_continuous_time

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

/--
The normalized total sojourn of jobs arrived by `t` converges to the product of
the arrival-rate limit and the Cesaro sojourn-time limit.
-/
theorem arrivedSojournRate_tendsto
    (q : ContinuousSamplePath) (lam Theta : ℝ)
    (hArrivalRate : Tendsto (empiricalArrivalRate q) atTop (𝓝 lam))
    (hSojournMean : Tendsto (averageSojourn q) atTop (𝓝 Theta)) :
    Tendsto (arrivedSojournRate q) atTop (𝓝 (lam * Theta)) := by
  -- Depends on:
  -- * `arrivalCount_at_arrival`
  -- * finite-prefix removal for Cesaro means
  -- * composition with `arrivalCount q t`
  sorry

/-! ## Non-FIFO boundary argument -/