timeAverageQueueLength_eventually_ge_scaled_product

import Definitions.Def_queueing_continuous_time

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

/--
The direct lower-bound form needed for the final squeeze: for every positive
`eps`, the area average is eventually at least arbitrarily close to
`(lam * Theta) / (1 + eps)`.
-/
theorem timeAverageQueueLength_eventually_ge_scaled_product
    (q : ContinuousSamplePath) (lam Theta eps delta : ℝ)
    (heps : 0 < eps) (hdelta : 0 < delta)
    (hArrivalRate : Tendsto (empiricalArrivalRate q) atTop (𝓝 lam))
    (hSojournMean : Tendsto (averageSojourn q) atTop (𝓝 Theta)) :
    ∀ᶠ t in atTop,
      (lam * Theta) / (1 + eps) - delta ≤ timeAverageQueueLength q t := by
  -- Depends on:
  -- * `scaled_tail_arrivedSojourn_le_departedSojourn_eventually`
  -- * `scaledArrivedTailSojournRate_tendsto`
  -- * `departedSojournRate_le_timeAverageQueueLength_eventually`
  sorry