scaledArrivedTailSojournRate_tendsto

import Definitions.Def_queueing_continuous_time

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

/--
After dropping finitely many jobs and replacing `t` by `t / (1 + eps)`, the
normalized arrived-sojourn sum converges to `(lam * Theta) / (1 + eps)`.
-/
theorem scaledArrivedTailSojournRate_tendsto
    (q : ContinuousSamplePath) (lam Theta eps : ℝ) (N : Nat)
    (heps : 0 < eps)
    (hArrivalRate : Tendsto (empiricalArrivalRate q) atTop (𝓝 lam))
    (hSojournMean : Tendsto (averageSojourn q) atTop (𝓝 Theta)) :
    Tendsto (scaledArrivedTailSojournRate q N eps) atTop
      (𝓝 ((lam * Theta) / (1 + eps))) := by
  -- Depends on:
  -- * `arrivedSojournRate_tendsto`
  -- * finite-prefix removal
  -- * composition with `t / (1 + eps)`
  sorry