Continuous paths in Skorokhod space

Continuous paths are càdlàg, and convergence to a continuous limit in the J1 topology implies uniform convergence.

theorem BGW.Skorokhod.bddAbove_displacement {T : ℝ} (hT : 0 ≤ T) (σ : TimeChange T) : BddAbove (Set.range fun (t : ↑(Set.Icc 0 T)) => |↑(σ t) - ↑t|)

The displacement of a time change on a compact interval is bounded.

theorem BGW.Skorokhod.displacement_nonneg {T : ℝ} (σ : TimeChange T) (hT : 0 ≤ T) : 0 ≤ ⨆ (t : ↑(Set.Icc 0 T)), |↑(σ t) - ↑t|

The supremum displacement of a time change is nonnegative.

theorem BGW.Skorokhod.bddAbove_comp_dist {E : Type u_1} [PseudoMetricSpace E] {T : ℝ} (hT : 0 ≤ T) (f g : D T E) (σ : TimeChange T) : BddAbove (Set.range fun (t : ↑(Set.Icc 0 T)) => dist (f (σ t)) (g t))

Distances between two càdlàg paths, with one composed with a time change, are bounded above.

def BGW.Skorokhod.ofContinuous {T : ℝ} {E : Type u_1} [TopologicalSpace E] (f : C(↑(Set.Icc 0 T), E)) : D T E

A continuous path, seen as a càdlàg path (C5).

Equations

• BGW.Skorokhod.ofContinuous f = { toFun := ⇑f, isCadlag' := ⋯ }

theorem BGW.Skorokhod.lipschitzWith_one_ofContinuous {T : ℝ} {E : Type u_1} [MetricSpace E] : LipschitzWith 1 ofContinuous

On continuous paths the J1 distance is at most the uniform distance (C5.1).

theorem BGW.Skorokhod.j1Dist_le_timeChange_cost {T : ℝ} {E : Type u_1} [PseudoMetricSpace E] (hT : 0 ≤ T) (f g : D T E) (σ : TimeChange T) : j1Dist f g ≤ max (⨆ (t : ↑(Set.Icc 0 T)), |↑(σ t) - ↑t|) (⨆ (t : ↑(Set.Icc 0 T)), dist (f t) (g (σ t)))

The J1 distance is at most the cost of any chosen time change.

theorem BGW.Skorokhod.tendsto_iSup_dist_of_tendsto_ofContinuous {T : ℝ} {E : Type u_1} [MetricSpace E] {ι : Type u_2} {l : Filter ι} {u : ι → D T E} {f : C(↑(Set.Icc 0 T), E)} (h : Filter.Tendsto u l (nhds (ofContinuous f))) : Filter.Tendsto (fun (i : ι) => ⨆ (t : ↑(Set.Icc 0 T)), dist ((u i) t) (f t)) l (nhds 0)

J1 convergence to a continuous path is uniform convergence (C5.2).