sojourn_div_arrival_tendsto_zero

import Definitions.Def_queueing_continuous_time

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

/--
Convergence of the arrival rate and Cesaro mean sojourn time implies that each
individual sojourn is negligible relative to its arrival epoch.
-/
theorem sojourn_div_arrival_tendsto_zero
    (q : ContinuousSamplePath) (lam Theta : ℝ)
    (hArrivalRate : Tendsto (empiricalArrivalRate q) atTop (𝓝 lam))
    (hSojournMean : Tendsto (averageSojourn q) atTop (𝓝 Theta)) :
    Tendsto (fun n => sojournTime q n / q.arrival n) atTop (𝓝 0) := by
  -- Depends on:
  -- * `sojourn_div_index_tendsto_zero`
  -- * `index_div_arrival_tendsto`
  sorry