Measurability of path maps

Restriction and fixed time–space scaling are measurable because the Borel σ-algebra is generated by path evaluations.

theorem BGW.Skorokhod.measurable_ofContinuous {T : ℝ} : Measurable ofContinuous

Continuous paths are Borel-measurably embedded in Skorokhod space.

theorem BGW.Skorokhod.measurable_restrict {T a : ℝ} (haT : a ≤ T) : Measurable (restrict haT)

Restriction of a Skorokhod path is Borel measurable.

theorem BGW.Skorokhod.measurable_timeSpaceScale_fixed {T : ℝ} (hT : 0 < T) {c : ℝ} (hc : 0 < c) (k : ℝ) : Measurable fun (f : D (c * T) ℝ) => timeSpaceScale T ⋯ (f, k, ⟨c, ⋯⟩)

Fixed horizon-to-horizon time–space scaling is Borel measurable.