Adapted evaluations at optional times

Stopping a path at a deterministic time gives a path-valued random variable measurable for that time's σ-algebra, by the cylinder characterization. Joint evaluation then gives measurability of evaluation at an optional time capped at that deterministic time. No regularity of the filtration is required.

theorem BGW.Skorokhod.IsOptionalTime.measurableSet_displacement {T : ℝ} {Ω : Type u_1} {m : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration (↑(Set.Icc 0 T)) m} {σ : Ω → ↑(Set.Icc 0 T)} (hσ : IsOptionalTime 𝓕 σ) (X : Ω → D T ℝ) (hadapted : ∀ (t : ↑(Set.Icc 0 T)), Measurable fun (ω : Ω) => (X ω) t) (t : ↑(Set.Icc 0 T)) (ε : ℝ) : MeasurableSet {ω : Ω | σ ω < t ∧ ε < |(X ω) t - (X ω) (σ ω)|}

A strict displacement at a deterministic time after an optional time is an adapted event.

Reference: Billingsley 1999, Section 16.