Transfer of Aldous bounds to optional times

Right continuity transfers uniform bounds at strictly rounded stopping times to optional times. Continuity from below applies to outer measures of increasing sets, so this step does not require a separate measurability argument for the events.

theorem BGW.Skorokhod.exists_uniform_aldous_optional_bound {T : ℝ} (hT : 0 < T) {Ω : ℕ → Type u_1} [m : (n : ℕ) → MeasurableSpace (Ω n)] (P : (n : ℕ) → MeasureTheory.Measure (Ω n)) (𝓕 : (n : ℕ) → MeasureTheory.Filtration (↑(Set.Icc 0 T)) (m n)) (X : (n : ℕ) → Ω n → D 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, ∃ (N : ℕ), ∀ n ≥ N, ∀ (σ : Ω n → ↑(Set.Icc 0 T)), IsOptionalTime (𝓕 n) σ → ∀ (h : ℝ), 0 ≤ h → h ≤ δ → (P n) {ω : Ω n | ε < |(X n ω) (Set.projIcc 0 T ⋯ (↑(σ ω) + h)) - (X n ω) (σ ω)|} ≤ ENNReal.ofReal η

Aldous's sequence condition gives a uniform strict-increment bound at optional times.

Reference: Billingsley 1999, Section 16.