Documentation

BGW.Skorokhod.Restrict

Evaluation, restriction and stopping on Skorokhod space #

This module proves continuity properties of evaluation and prepares the restriction and stopping operations on compact intervals.

source
theorem BGW.Skorokhod.lipschitzWith_one_eval_zero {T : ℝ} {E : Type u_1} [MetricSpace E] (hT : 0 ≤ T) :
LipschitzWith 1 fun (f : D T E) => f ⟨0, ⋯⟩

Evaluation at time 0 is 1-Lipschitz (C6.1).

source
theorem BGW.Skorokhod.lipschitzWith_one_eval_right {T : ℝ} {E : Type u_1} [MetricSpace E] (hT : 0 ≤ T) :
LipschitzWith 1 fun (f : D T E) => f ⟨T, ⋯⟩

Evaluation at the terminal time T is 1-Lipschitz (C6.1).

source
theorem BGW.Skorokhod.continuousAt_eval {T : ℝ} {E : Type u_1} [MetricSpace E] {f : D T E} {t : ↑(Set.Icc 0 T)} (hf : ContinuousAt (⇑f) t) :
ContinuousAt (fun (g : D T E) => g t) f

Evaluation at t is continuous at every path continuous at t (C6.1).

source
def BGW.Skorokhod.restrict {T : ℝ} {E : Type u_1} [TopologicalSpace E] {a : ℝ} (haT : a ≤ T) (f : D T E) :
D a E

Restriction of a path on [0,T] to [0,a] (C6.2).

Equations
Instances For
    source
    def BGW.Skorokhod.extendConst {T : ℝ} {E : Type u_1} [TopologicalSpace E] {a : ℝ} (ha : 0 ≤ a) (haT : a ≤ T) (g : D a E) :
    D T E

    Constant extension of a path on [0,a] to [0,T]: t ↦ g (min t a) (C6.2).

    Equations
    Instances For
      source
      theorem BGW.Skorokhod.lipschitzWith_one_extendConst {T : ℝ} {E : Type u_1} [MetricSpace E] {a : ℝ} (ha : 0 ≤ a) (haT : a ≤ T) :
      LipschitzWith 1 (extendConst ha haT)

      Constant extension is 1-Lipschitz (C6.2).

      source
      def BGW.Skorokhod.stop {T : ℝ} {E : Type u_1} [TopologicalSpace E] (a : ℝ) (f : D T E) :
      D T E

      The path stopped at time a: t ↦ f (max 0 (min t a)); total in a (C6.2).

      Equations
      Instances For
        source
        theorem BGW.Skorokhod.stop_eq_extendConst_restrict {T : ℝ} {E : Type u_1} [TopologicalSpace E] {a : ℝ} (ha : 0 ≤ a) (haT : a ≤ T) (f : D T E) :
        stop a f = extendConst ha haT (restrict haT f)

        For 0 ≤ a ≤ T, stopping is extension after restriction (C6.2).

        source
        theorem BGW.Skorokhod.dist_stop_le {T : ℝ} {E : Type u_1} [MetricSpace E] {a : ℝ} (ha : 0 ≤ a) (haT : a ≤ T) (f : D T E) :
        dist (stop a f) f ≤ ⨆ (s : { s : ↑(Set.Icc 0 T) // a ≤ ↑s }), dist (f ↑s) (f ⟨a, ⋯⟩)

        Stopped-path approximation (C7).

        source
        theorem BGW.Skorokhod.tendsto_stop_nhdsLT {T : ℝ} {E : Type u_1} [MetricSpace E] (hT : 0 < T) {f : D T E} (hf : ContinuousAt ⇑f ⟨T, ⋯⟩) :
        Filter.Tendsto (fun (a : ℝ) => stop a f) (nhdsWithin T (Set.Iio T)) (nhds f)

        A path continuous at the terminal time is the J1 limit of its stopped paths (C7).

        source
        theorem BGW.Skorokhod.lipschitzWith_one_iInf {T : ℝ} (hT : 0 ≤ T) :
        LipschitzWith 1 fun (f : D T ℝ) => ⨅ (t : ↑(Set.Icc 0 T)), f t

        The infimum of a real path is 1-Lipschitz for J1 (C6.3).

        source
        theorem BGW.Skorokhod.lipschitzWith_one_iSup {T : ℝ} (hT : 0 ≤ T) :
        LipschitzWith 1 fun (f : D T ℝ) => ⨆ (t : ↑(Set.Icc 0 T)), f t

        The supremum of a real path is 1-Lipschitz for J1 (C6.3).