Optional results on Skorokhod space

This module proves the continuous-locus converse for pairing paths, restriction and stopping in continuous path space, the signed jump and localization of the Vervaat wrap, and attainment and characterizations of the largest upward jump.

def BGW.Skorokhod.fstWithCont {T : ℝ} {E : Type u_1} {F : Type u_2} [MetricSpace E] [MetricSpace F] (f : D T (E × F)) : D T E

First coordinate of a product-valued càdlàg path.

Equations

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

noncomputable def BGW.Skorokhod.splitProdWithCont {T : ℝ} {E : Type u_1} {F : Type u_2} [MetricSpace E] [MetricSpace F] [Inhabited F] (f : D T (E × F)) : D T E × C(↑(Set.Icc 0 T), F)

Split a product-valued path when its second coordinate is continuous. Outside that locus, use the constant continuous path default as an explicit junk value.

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.Skorokhod.tendsto_map_splitProdWithCont {T : ℝ} {E : Type u_1} {F : Type u_2} [MetricSpace E] [MetricSpace F] [Inhabited F] [TopologicalSpace.SeparableSpace F] {μ : ℕ → MeasureTheory.ProbabilityMeasure (D T (E × F))} {ν : MeasureTheory.ProbabilityMeasure (D T (E × F))} (hlim : Filter.Tendsto μ Filter.atTop (nhds ν)) (hμ : ∀ (n : ℕ), ∀ᵐ (f : D T (E × F)) ∂↑(μ n), Continuous fun (t : ↑(Set.Icc 0 T)) => (f t).2) (hν : ∀ᵐ (f : D T (E × F)) ∂↑ν, Continuous fun (t : ↑(Set.Icc 0 T)) => (f t).2) : Filter.Tendsto (fun (n : ℕ) => (μ n).map splitProdWithCont) Filter.atTop (nhds (ν.map splitProdWithCont))

C5 item 4, converse. Convergence in law in D_T(E × F), on the locus where the second coordinate is continuous, implies convergence in law in D_T(E) × C([0,T],F).

theorem BGW.Skorokhod.prodWithCont_splitProdWithCont {T : ℝ} {E : Type u_1} {F : Type u_2} [MetricSpace E] [MetricSpace F] [Inhabited F] (f : D T (E × F)) (hf : Continuous fun (t : ↑(Set.Icc 0 T)) => (f t).2) : prodWithCont (splitProdWithCont f).1 (splitProdWithCont f).2 = f

Splitting followed by prodWithCont is the identity on paths with continuous second coordinate.

def BGW.Skorokhod.restrictContinuous {T : ℝ} {E : Type u_1} [MetricSpace E] {a : ℝ} (haT : a ≤ T) (f : C(↑(Set.Icc 0 T), E)) : C(↑(Set.Icc 0 a), E)

Restriction of a continuous path to [0,a].

Equations

• BGW.Skorokhod.restrictContinuous haT f = f.comp { toFun := fun (t : ↑(Set.Icc 0 a)) => ⟨↑t, ⋯⟩, continuous_toFun := ⋯ }

def BGW.Skorokhod.extendContinuous {T : ℝ} {E : Type u_1} [MetricSpace E] {a : ℝ} (ha : 0 ≤ a) (f : C(↑(Set.Icc 0 a), E)) : C(↑(Set.Icc 0 T), E)

Extend a continuous path on [0,a] constantly to [0,T].

Equations

• BGW.Skorokhod.extendContinuous ha f = f.comp { toFun := fun (t : ↑(Set.Icc 0 T)) => ⟨min (↑t) a, ⋯⟩, continuous_toFun := ⋯ }

def BGW.Skorokhod.stopContinuous {T : ℝ} {E : Type u_1} [MetricSpace E] (a : ℝ) (f : C(↑(Set.Icc 0 T), E)) : C(↑(Set.Icc 0 T), E)

Stop a continuous path at a, with the same clamped-time convention as Skorokhod.stop.

Equations

• BGW.Skorokhod.stopContinuous a f = f.comp { toFun := fun (t : ↑(Set.Icc 0 T)) => ⟨max 0 (min (↑t) a), ⋯⟩, continuous_toFun := ⋯ }

theorem BGW.Skorokhod.lipschitzWith_one_restrictContinuous {T : ℝ} {E : Type u_1} [MetricSpace E] {a : ℝ} (haT : a ≤ T) : LipschitzWith 1 (restrictContinuous haT)

Restricting a continuous path to an initial interval is 1-Lipschitz.

theorem BGW.Skorokhod.lipschitzWith_one_extendContinuous {T : ℝ} {E : Type u_1} [MetricSpace E] {a : ℝ} (ha : 0 ≤ a) : LipschitzWith 1 (extendContinuous ha)

Constant extension of a continuous path is 1-Lipschitz.

theorem BGW.Skorokhod.lipschitzWith_one_stopContinuous {T : ℝ} {E : Type u_1} [MetricSpace E] (a : ℝ) : LipschitzWith 1 (stopContinuous a)

Stopping a continuous path is 1-Lipschitz.

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

C7 in C_T. Stopping at a is controlled by the uniform oscillation after a.

theorem BGW.Skorokhod.tendsto_continuous_of_tendsto_restrict_of_oscillation {T : ℝ} {E : Type u_1} [MetricSpace E] {Ω : ℕ → Type u_3} [(n : ℕ) → MeasurableSpace (Ω n)] [TopologicalSpace.SeparableSpace E] (μ : (n : ℕ) → MeasureTheory.ProbabilityMeasure (Ω n)) {Y : (n : ℕ) → Ω n → C(↑(Set.Icc 0 T), E)} (hY : ∀ (n : ℕ), Measurable (Y n)) {ν : MeasureTheory.ProbabilityMeasure C(↑(Set.Icc 0 T), E)} (hT : 0 < T) {a : ℕ → ℝ} (ha0 : ∀ (k : ℕ), 0 ≤ a k) (haT : ∀ (k : ℕ), a k < T) (hlim : Filter.Tendsto a Filter.atTop (nhds T)) (hpre : ∀ (k : ℕ), Filter.Tendsto (fun (n : ℕ) => (μ n).map (restrictContinuous ⋯ ∘ Y n)) Filter.atTop (nhds (ν.map (restrictContinuous ⋯)))) (hosc : ∀ η > 0, Filter.Tendsto (fun (k : ℕ) => Filter.limsup (fun (n : ℕ) => (↑(μ n)).real {ω : Ω n | η < ⨆ (s : { s : ↑(Set.Icc 0 T) // a k ≤ ↑s }), dist ((Y n ω) ↑s) ((Y n ω) ⟨a k, ⋯⟩)}) Filter.atTop) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => (μ n).map (Y n)) Filter.atTop (nhds ν)

C11 item 2 in C_T. Convergence of continuous prefixes and terminal oscillation control imply convergence in law on the full continuous path space.

noncomputable def BGW.Skorokhod.vervaatWrapTime (f : D 1 ℝ) : ↑(Set.Icc 0 1)

The wrap time 1 - g, viewed as a point of [0,1].

Equations

• BGW.Skorokhod.vervaatWrapTime f = Set.projIcc 0 1 BGW.Skorokhod.vervaatWrapTime._proof_1 (1 - ↑(BGW.Skorokhod.vervaatTime f))

theorem BGW.Skorokhod.vervaatD_wrap (f : D 1 ℝ) : (vervaatD f) (vervaatWrapTime f) = f ⟨1, ⋯⟩ - ⨅ (s : ↑(Set.Icc 0 1)), f s

Value of the Vervaat transform at its wrap time.

theorem BGW.Skorokhod.leftLim_vervaatD_wrap (f : D 1 ℝ) (hc : 0 < ↑(vervaatWrapTime f)) : Function.leftLim (⇑(vervaatD f)) (vervaatWrapTime f) = Function.leftLim ⇑f ⟨1, ⋯⟩ - ⨅ (s : ↑(Set.Icc 0 1)), f s

Left limit of the Vervaat transform at its wrap time.

theorem BGW.Skorokhod.vervaatD_wrap_sub_leftLim (f : D 1 ℝ) (hc : 0 < ↑(vervaatWrapTime f)) : (vervaatD f) (vervaatWrapTime f) - Function.leftLim (⇑(vervaatD f)) (vervaatWrapTime f) = f ⟨1, ⋯⟩ - Function.leftLim ⇑f ⟨1, ⋯⟩

C33 item 3b. The signed jump at the wrap is f(1) - f(1-).

theorem BGW.Skorokhod.vervaatD_jump_of_ne_wrap (f : D 1 ℝ) (t : ↑(Set.Icc 0 1)) (ht0 : 0 < ↑t) (htc : t ≠ vervaatWrapTime f) : (vervaatD f) t - Function.leftLim (⇑(vervaatD f)) t = f (Set.projIcc 0 1 ⋯ (if ↑(vervaatTime f) + ↑t < 1 then ↑(vervaatTime f) + ↑t else ↑(vervaatTime f) + ↑t - 1)) - Function.leftLim (⇑f) (Set.projIcc 0 1 ⋯ (if ↑(vervaatTime f) + ↑t < 1 then ↑(vervaatTime f) + ↑t else ↑(vervaatTime f) + ↑t - 1))

C33 item 3b, localization (audit g3, finding 2): away from the wrap time, the jump of the Vervaat transform at t > 0 is the jump of f at the rotated time g + t (mod 1).

theorem BGW.Skorokhod.exists_eq_maxJump {T : ℝ} (hT : 0 ≤ T) (f : D T ℝ) : ∃ (t : ↑(Set.Icc 0 T)), max (f t - Function.leftLim (⇑f) t) 0 = maxJump f

C36, attainment. On a nonempty bounded time interval, maxJump is attained.

theorem BGW.Skorokhod.maxJump_eq_zero_iff {T : ℝ} (f : D T ℝ) : maxJump f = 0 ↔ ∀ (t : ↑(Set.Icc 0 T)), f t ≤ Function.leftLim (⇑f) t

The exact meaning of maxJump f = 0: there are no upward jumps. Downward jumps are invisible to maxJump.