Cylinder generation of the Skorokhod Borel structure

For a complete state space, countable dense evaluations give a Borel embedding. An isometric embedding into the completion removes the completeness assumption.

theorem BGW.Skorokhod.eq_of_eval_eq_on_dense {T : ℝ} {E : Type u_1} [MetricSpace E] {S : Set ↑(Set.Icc 0 T)} (hS : Dense S) (hT0 : 0 ≤ T) (hTS : ⟨T, ⋯⟩ ∈ S) {f g : D T E} (hfg : ∀ t ∈ S, f t = g t) : f = g

Dense evaluations, including the terminal evaluation, determine a càdlàg path.

def BGW.Skorokhod.toCompletion {T : ℝ} {E : Type u_1} [MetricSpace E] (f : D T E) : D T (UniformSpace.Completion E)

Applying the canonical embedding into the completion to every path value.

Equations

• BGW.Skorokhod.toCompletion f = { toFun := fun (t : ↑(Set.Icc 0 T)) => ↑(f t), isCadlag' := ⋯ }

theorem BGW.Skorokhod.isometry_toCompletion {T : ℝ} {E : Type u_1} [MetricSpace E] : Isometry toCompletion

The embedding of paths into the completion preserves the J1 distance.

theorem BGW.Skorokhod.measurableSpace_eq_iSup_comap_eval {T : ℝ} {E : Type u_1} [MetricSpace E] [TopologicalSpace.SeparableSpace E] [MeasurableSpace E] [BorelSpace E] {S : Set ↑(Set.Icc 0 T)} (hS : Dense S) (hT0 : 0 ≤ T) (hTS : ⟨T, ⋯⟩ ∈ S) : inferInstance = ⨆ t ∈ S, MeasurableSpace.comap (fun (f : D T E) => f t) inst✝

For separable E, the Borel σ-algebra of D is generated by the evaluations at the times of any dense set containing the terminal time (Billingsley 1999, Theorem 12.5; C4.2).