Determination and convergence of path laws from prefixes

Stopped paths approximate a path near the terminal time. We use this approximation to prove weak convergence from convergence of restrictions and uniqueness of laws with equal prefixes.

theorem BGW.Skorokhod.measurable_restrict_of_nonneg {T : ℝ} {E : Type u_1} [MetricSpace E] [TopologicalSpace.SeparableSpace E] {a : ℝ} (ha : 0 ≤ a) (haT : a ≤ T) : Measurable (restrict haT)

Restriction to a nonnegative prefix is Borel measurable for the J1 Borel structures.

theorem BGW.Skorokhod.measurable_stop_of_nonneg {T : ℝ} {E : Type u_1} [MetricSpace E] [TopologicalSpace.SeparableSpace E] {a : ℝ} (ha : 0 ≤ a) (haT : a ≤ T) : Measurable (stop a)

Stopping at a time in [0, T] is Borel measurable for the J1 Borel structures.

theorem BGW.Skorokhod.tendsto_map_stop {T : ℝ} {E : Type u_1} [MetricSpace E] [TopologicalSpace.SeparableSpace E] {P : MeasureTheory.ProbabilityMeasure (D T E)} (hT : 0 < T) {a : ℕ → ℝ} (ha0 : ∀ (k : ℕ), 0 ≤ a k) (haT : ∀ (k : ℕ), a k < T) (hlim : Filter.Tendsto a Filter.atTop (nhds T)) (hcont : ∀ᵐ (f : D T E) ∂↑P, ContinuousAt ⇑f ⟨T, ⋯⟩) : Filter.Tendsto (fun (k : ℕ) => P.map (stop (a k))) Filter.atTop (nhds P)

Stopped laws converge weakly to the original law along times increasing to the terminal time, provided the original law is almost surely continuous there.

theorem BGW.Skorokhod.map_extendConst_restrict {T : ℝ} {E : Type u_1} [MetricSpace E] [TopologicalSpace.SeparableSpace E] (P : MeasureTheory.ProbabilityMeasure (D T E)) {a : ℝ} (ha : 0 ≤ a) (haT : a ≤ T) : (P.map (restrict haT)).map (extendConst ha haT) = P.map (stop a)

Constant extension after restriction is the same operation on laws as stopping.

theorem BGW.Skorokhod.tendsto_of_tendsto_restrict_of_oscillation {T : ℝ} {E : Type u_1} {Ω : ℕ → Type u_2} [(n : ℕ) → MeasurableSpace (Ω n)] [MetricSpace E] [TopologicalSpace.SeparableSpace E] (μ : (n : ℕ) → MeasureTheory.ProbabilityMeasure (Ω n)) {Y : (n : ℕ) → Ω n → D T E} (hY : ∀ (n : ℕ), Measurable (Y n)) {ν : MeasureTheory.ProbabilityMeasure (D 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 (restrict ⋯ ∘ Y n)) Filter.atTop (nhds (ν.map (restrict ⋯)))) (hcont : ∀ᵐ (f : D T E) ∂↑ν, ContinuousAt ⇑f ⟨T, ⋯⟩) (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 ν)

Convergence in law in D from convergence of the restrictions to [0, a k] for times a k ↑ T, a limit almost surely continuous at T, and control of the oscillation after a k (Billingsley 1999, Theorem 3.2 with C7; C11(2)).

theorem BGW.Skorokhod.ext_of_restrict {T : ℝ} {E : Type u_1} [MetricSpace E] [TopologicalSpace.SeparableSpace E] {P Q : MeasureTheory.ProbabilityMeasure (D T E)} (hT : 0 < T) {a : ℕ → ℝ} (haT : ∀ (k : ℕ), a k < T) (hlim : Filter.Tendsto a Filter.atTop (nhds T)) (hP : ∀ᵐ (f : D T E) ∂↑P, ContinuousAt ⇑f ⟨T, ⋯⟩) (hQ : ∀ᵐ (f : D T E) ∂↑Q, ContinuousAt ⇑f ⟨T, ⋯⟩) (h : ∀ (k : ℕ), P.map (restrict ⋯) = Q.map (restrict ⋯)) : P = Q

Two laws on D, both almost surely continuous at T, with equal restrictions to [0, a k] for times a k ↑ T, are equal (C12(2)).