eventually_departure_le_scaled_arrival

import Definitions.Def_queueing_continuous_time

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

/--
For every positive `eps`, all sufficiently late jobs satisfy
`departure n ≤ (1 + eps) * arrival n`.
-/
theorem eventually_departure_le_scaled_arrival
    (q : ContinuousSamplePath) (lam Theta eps : ℝ)
    (heps : 0 < eps)
    (hArrivalRate : Tendsto (empiricalArrivalRate q) atTop (𝓝 lam))
    (hSojournMean : Tendsto (averageSojourn q) atTop (𝓝 Theta)) :
    ∀ᶠ n in atTop, q.departure n ≤ (1 + eps) * q.arrival n := by
  -- Depends on `sojourn_div_arrival_tendsto_zero`.
  sorry