Finite deterministic control times

A finite net of the time interval meets every block of a partition whose gaps exceed δ. A modulus bound therefore turns bounds at finitely many deterministic times, including the horizon, into a bound at every time.

theorem BGW.Skorokhod.exists_finite_aldous_control_times {T : ℝ} (hT : 0 < T) {δ : ℝ} (hδ : 0 < δ) (hδT : δ < T) : ∃ (S : Set ↑(Set.Icc 0 T)), S.Finite ∧ ∀ (f : D T ℝ) (c : ℝ), (∀ t ∈ S, |f t| ≤ c) → cadlagModulus f δ ≤ 1 → ∀ (t : ↑(Set.Icc 0 T)), |f t| ≤ c + 2

A fixed finite set of time evaluations controls the supremum of every path with cadlagModulus f δ ≤ 1.

Reference: Billingsley 1999, Section 16.