index_div_arrival_tendsto

Proved

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

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

Formal statement

import Definitions.Def_queueing_continuous_time

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

/--
Sampling the empirical arrival-rate limit at arrival epochs gives
`n / arrival n → lam`. The zero-based `+ 1` discrepancy vanishes.
-/
theorem index_div_arrival_tendsto
    (q : ContinuousSamplePath) (lam : ℝ)
    (hArrivalRate : Tendsto (empiricalArrivalRate q) atTop (𝓝 lam)) :
    Tendsto (fun n : Nat => (n : ℝ) / q.arrival n) atTop (𝓝 lam) := by
  -- Depends on:
  -- * `arrival_tendsto_atTop`
  -- * `arrivalCount_at_arrival`
  sorry

Source

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

View graph