departedSojourn_le_queueArea

import Definitions.Def_queueing_continuous_time

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

/--
The total full sojourn of jobs departed by `t` is bounded above by the area
under the queue-length path through `t`.
-/
theorem departedSojourn_le_queueArea
    (q : ContinuousSamplePath) (t : ℝ) (ht : 0 ≤ t) :
    (∑ n ∈ departedBy q t, sojournTime q n) ≤
      ∫ s in (0 : ℝ)..t, (queueLength q s : ℝ) := by
  -- Depends on:
  -- * `mem_departedBy`
  -- * `intervalIntegrable_queueLength`
  -- * `sojournTime_nonneg`
  sorry