Aldous's uniform modulus estimate

First bound the number of genuine exits in probability. Then exclude short gaps among a fixed finite number of exits and control a deterministic terminal window. Merging the last block produces a partition admissible for Billingsley's modulus.

theorem BGW.Skorokhod.exists_uniform_aldous_modulus_bound {T : ℝ} (hT : 0 < T) {Ω : ℕ → Type u_1} [m : (n : ℕ) → MeasurableSpace (Ω n)] (P : (n : ℕ) → MeasureTheory.Measure (Ω n)) [∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (P n)] (𝓕 : (n : ℕ) → MeasureTheory.Filtration (↑(Set.Icc 0 T)) (m n)) (X : (n : ℕ) → Ω n → D T ℝ) (hX : ∀ (n : ℕ), Measurable (X n)) (hadapted : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)), Measurable fun (ω : Ω n) => (X n ω) t) (hAldous : ∀ (τ : (n : ℕ) → Ω n → ↑(Set.Icc 0 T)), (∀ (n : ℕ), IsStopTime (𝓕 n) (τ n)) → ∀ (h : ℕ → ℝ), (∀ (n : ℕ), 0 ≤ h n) → Filter.Tendsto h Filter.atTop (nhds 0) → ∀ ε > 0, Filter.Tendsto (fun (n : ℕ) => (P n) {ω : Ω n | ε ≤ |(X n ω) (Set.projIcc 0 T ⋯ (↑(τ n ω) + h n)) - (X n ω) (τ n ω)|}) Filter.atTop (nhds 0)) {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) : ∃ (δ : ℝ), 0 < δ ∧ δ < T ∧ ∃ (N : ℕ), ∀ n ≥ N, (P n) {ω : Ω n | ε < cadlagModulus (X n ω) δ} ≤ ENNReal.ofReal η

Aldous's sequence condition makes the modulus small in probability for all large indices.

Reference: Billingsley 1999, Section 16.