arrivalCount_at_arrival

Proved

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

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

Formal statement

import Definitions.Def_queueing_continuous_time

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

/-- With zero-based indexing, exactly `n + 1` jobs have arrived by `arrival n`. -/
theorem arrivalCount_at_arrival (q : ContinuousSamplePath) (n : Nat) :
    arrivalCount q (q.arrival n) = n + 1 := 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