timeAverageQueueLength_le_arrivedSojournRate_eventually

Proved

by wenxinzhang · Jul 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

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

Formal statement

import Definitions.Def_queueing_continuous_time

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

/-- The normalized arrived-sojourn total eventually bounds the time average above. -/
theorem timeAverageQueueLength_le_arrivedSojournRate_eventually
    (q : ContinuousSamplePath) :
    ∀ᶠ t in atTop,
      timeAverageQueueLength q t ≤ arrivedSojournRate q t := by
  -- Depends on `queueArea_le_arrivedSojourn`.
  sorry

/-! ## Arrival-rate and Cesaro-sojourn asymptotics -/

Source

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

View graph