exists_tail_arrivedBy_scaled_subset_departedBy

import Definitions.Def_queueing_continuous_time

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

/--
For every positive `eps`, there is a finite initial set of exceptional jobs
such that, eventually in `t`, every later job that arrived by `t / (1 + eps)`
has departed by `t`.
-/
theorem exists_tail_arrivedBy_scaled_subset_departedBy
    (q : ContinuousSamplePath) (lam Theta eps : ℝ)
    (heps : 0 < eps)
    (hArrivalRate : Tendsto (empiricalArrivalRate q) atTop (𝓝 lam))
    (hSojournMean : Tendsto (averageSojourn q) atTop (𝓝 Theta)) :
    ∃ N : Nat, ∀ᶠ t in atTop,
      ∀ n : Nat, N ≤ n →
        n ∈ q.arrivedBy (t / (1 + eps)) →
          n ∈ departedBy q t := by
  -- Depends on:
  -- * `eventually_departure_le_scaled_arrival`
  -- * `mem_departedBy`
  sorry