sojourn_div_index_tendsto_zero

Proved

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

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

Formal statement

import Definitions.Def_queueing_continuous_time

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

/--
If the Cesaro means of the sojourn sequence converge, individual sojourn times
are sublinear in the job index.
-/
theorem sojourn_div_index_tendsto_zero
    (q : ContinuousSamplePath) (Theta : ℝ)
    (hSojournMean : Tendsto (averageSojourn q) atTop (𝓝 Theta)) :
    Tendsto (fun n : Nat => sojournTime q n / (n : ℝ)) atTop (𝓝 0) := by
  -- Depends on a standard Cesaro-difference lemma for convergent averages.
  sorry

Source

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

View graph