timeAverageQueueLength_tendsto_of_scaled_lower_and_upper

import Definitions.Def_queueing_continuous_time

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

/--
The final squeeze step, stated in the form produced by the proof above. The
upper side comes from arrived sojourns by `t`; the lower side comes from arrived
sojourns by `t / (1 + eps)` after discarding finitely many jobs.
-/
theorem timeAverageQueueLength_tendsto_of_scaled_lower_and_upper
    (q : ContinuousSamplePath) (x : ℝ)
    (hx : 0 ≤ x)
    (hLower : ∀ eps : ℝ, 0 < eps → ∀ delta : ℝ, 0 < delta →
      ∀ᶠ t in atTop, x / (1 + eps) - delta ≤ timeAverageQueueLength q t)
    (hUpper : ∀ delta : ℝ, 0 < delta →
      ∀ᶠ t in atTop, timeAverageQueueLength q t ≤ x + delta) :
    Tendsto (timeAverageQueueLength q) atTop (𝓝 x) := by
  -- Depends on a real-analysis squeeze argument with the parameter `eps ↓ 0`.
  sorry