timeAverageQueueLength_eventually_le_product_add

import Definitions.Def_queueing_continuous_time

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

/--
The direct upper-bound form needed for the final squeeze: the area average is
eventually no larger than an arbitrary neighborhood above `lam * Theta`.
-/
theorem timeAverageQueueLength_eventually_le_product_add
    (q : ContinuousSamplePath) (lam Theta : ℝ)
    (delta : ℝ) (hdelta : 0 < delta)
    (hArrivalRate : Tendsto (empiricalArrivalRate q) atTop (𝓝 lam))
    (hSojournMean : Tendsto (averageSojourn q) atTop (𝓝 Theta)) :
    ∀ᶠ t in atTop,
      timeAverageQueueLength q t ≤ lam * Theta + delta := by
  -- Depends on:
  -- * `timeAverageQueueLength_le_arrivedSojournRate_eventually`
  -- * `arrivedSojournRate_tendsto`
  sorry