Documentation

BGW.Skorokhod.Postcomp

Postcomposition of càdlàg paths #

Postcomposition by a continuous map preserves càdlàg paths. It is continuous for the J1 topology: a convergent sequence of paths is eventually spatially close to the compact closure of the range of its limit, where Heine--Cantor gives uniform control. In particular, postcomposition is Borel measurable. A spatial K-Lipschitz map gives a J1 Lipschitz bound with constant max K 1; the time-displacement part of J1 is not compressed when K < 1.

source
def BGW.Skorokhod.D.postcomp {T : ℝ} {E : Type u_1} {F : Type u_2} [TopologicalSpace E] [TopologicalSpace F] (g : C(E, F)) :
D T E → D T F

Postcompose a càdlàg path by a continuous map.

Equations
Instances For
    source
    @[simp]
    theorem BGW.Skorokhod.D.postcomp_apply {T : ℝ} {E : Type u_1} {F : Type u_2} [TopologicalSpace E] [TopologicalSpace F] (g : C(E, F)) (f : D T E) (t : ↑(Set.Icc 0 T)) :
    (postcomp g f) t = g (f t)

    Postcomposition evaluates pointwise.

    source
    @[simp]
    theorem BGW.Skorokhod.D.postcomp_id {T : ℝ} {E : Type u_1} [TopologicalSpace E] (f : D T E) :
    postcomp (ContinuousMap.id E) f = f

    Postcomposition by the identity is the identity on càdlàg paths.

    source
    @[simp]
    theorem BGW.Skorokhod.D.postcomp_comp {T : ℝ} {E : Type u_1} {F : Type u_2} {G : Type u_3} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] (g : C(E, F)) (h : C(F, G)) (f : D T E) :
    postcomp (h.comp g) f = postcomp h (postcomp g f)

    Postcomposition respects composition of continuous maps.

    source
    theorem BGW.Skorokhod.D.continuous_postcomp {T : ℝ} {E : Type u_1} {F : Type u_2} [MetricSpace E] [MetricSpace F] (g : C(E, F)) :
    Continuous (postcomp g)

    Postcomposition by a continuous map is continuous for the Skorokhod J1 topology.

    source
    theorem BGW.Skorokhod.D.measurable_postcomp {T : ℝ} {E : Type u_1} {F : Type u_2} [MetricSpace E] [MetricSpace F] (g : C(E, F)) :
    Measurable (postcomp g)

    Postcomposition is Borel measurable.

    source
    theorem BGW.Skorokhod.D.lipschitzWith_postcomp {T : ℝ} {E : Type u_1} {F : Type u_2} [MetricSpace E] [MetricSpace F] {K : NNReal} {g : C(E, F)} (hg : LipschitzWith K ⇑g) :
    LipschitzWith (max K 1) (postcomp g)

    A spatial Lipschitz map is J1 Lipschitz after postcomposition, with constant max K 1. The 1 accounts for the unchanged time-displacement component of the J1 cost.