Prove2Me

intervalIntegrable_queueLength

Open

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

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

Formal statement
import Definitions.Def_queueing_continuous_time

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

/-- The real-valued queue-length path is integrable on every finite interval. -/
theorem intervalIntegrable_queueLength
    (q : ContinuousSamplePath) (t : ℝ) :
    IntervalIntegrable (fun s : ℝ => (queueLength q s : ℝ))
      MeasureTheory.volume 0 t := by
  sorry
Source
QueueingLib deterministic continuous-time Little's Law project. Root theorem: general_littles_law, theorem_id 81236938-cf7e-49ad-a078-be9ba5432532.

View graph