queueArea_le_arrivedSojourn

Open

by wenxinzhang · Jul 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

Supporting subproblem for the deterministic continuous-time Little's Law decomposition graph: queueArea_le_arrivedSojourn.

Formal statement

import Definitions.Def_queueing_continuous_time

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

/--
The queue area through `t` is bounded above by the total full sojourn of jobs
that have arrived by `t`.
-/
theorem queueArea_le_arrivedSojourn
    (q : ContinuousSamplePath) (t : ℝ) (ht : 0 ≤ t) :
    (∫ s in (0 : ℝ)..t, (queueLength q s : ℝ)) ≤
      ∑ n ∈ q.arrivedBy t, sojournTime q n := by
  -- Depends on:
  -- * `intervalIntegrable_queueLength`
  -- * `sojournTime_nonneg`
  sorry

Source

QueueingLib deterministic continuous-time Little's Law project. Root theorem: general_littles_law, theorem_id 81236938-cf7e-49ad-a078-be9ba5432532.

View graph