scaled_tail_arrivedSojourn_le_departedSojourn_eventually

import Definitions.Def_queueing_continuous_time

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

/--
The boundary inclusion turns into the lower sojourn-sum inequality used in the
proof: the departed-sojourn total by `t` dominates the tail of jobs that arrived
by `t / (1 + eps)`.
-/
theorem scaled_tail_arrivedSojourn_le_departedSojourn_eventually
    (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,
      arrivedTailSojourn q N (t / (1 + eps)) ≤
        ∑ n ∈ departedBy q t, sojournTime q n := by
  -- Depends on:
  -- * `exists_tail_arrivedBy_scaled_subset_departedBy`
  -- * `sojournTime_nonneg`
  sorry