Polishness and tightness criteria on Skorokhod space

This file proves Polishness and standard Borelness of D, specializes Skorokhod representation and Prokhorov's theorem to D, and gives Billingsley's compactness and tightness criteria in terms of bounded values and the càdlàg modulus.

References

• P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999, Sections 5, 6, 12 and 13.

theorem BGW.Skorokhod.polishSpace_D {T : ℝ} {E : Type u_1} [MetricSpace E] [CompleteSpace E] [TopologicalSpace.SeparableSpace E] : PolishSpace (D T E)

D([0,T], E) is Polish for complete separable metric E (Billingsley 1999, Theorems 12.1-12.2).

theorem BGW.Skorokhod.standardBorelSpace_D {T : ℝ} {E : Type u_1} [MetricSpace E] [CompleteSpace E] [TopologicalSpace.SeparableSpace E] : StandardBorelSpace (D T E)

D([0,T], E) with its Borel σ-algebra is a standard Borel space.

theorem BGW.Skorokhod.exists_tendsto_ae_of_tendsto_D {T : ℝ} {E : Type u_1} [MetricSpace E] [CompleteSpace E] [TopologicalSpace.SeparableSpace E] {P : ℕ → MeasureTheory.ProbabilityMeasure (D T E)} {Q : MeasureTheory.ProbabilityMeasure (D T E)} (h : Filter.Tendsto P Filter.atTop (nhds Q)) : ∃ (X : ℕ → ↑unitInterval → D T E) (Y : ↑unitInterval → D T E), (∀ (n : ℕ), Measurable (X n)) ∧ Measurable Y ∧ (∀ (n : ℕ), MeasureTheory.Measure.map (X n) MeasureTheory.volume = ↑(P n)) ∧ MeasureTheory.Measure.map Y MeasureTheory.volume = ↑Q ∧ ∀ᵐ (ω : ↑unitInterval), Filter.Tendsto (fun (n : ℕ) => X n ω) Filter.atTop (nhds (Y ω))

Skorokhod representation on D (Billingsley 1999, Theorem 6.7): weakly convergent laws on D([0,T], E) are the laws of random variables on ([0,1], Lebesgue) converging almost surely. Corollary of BGW.Probability.exists_tendsto_ae_of_tendsto and polishSpace_D.

theorem BGW.Skorokhod.isTightMeasureSet_iff_isCompact_closure_D {T : ℝ} {E : Type u_1} [MetricSpace E] [CompleteSpace E] [TopologicalSpace.SeparableSpace E] (S : Set (MeasureTheory.ProbabilityMeasure (D T E))) : MeasureTheory.IsTightMeasureSet {x : MeasureTheory.Measure (D T E) | ∃ μ ∈ S, ↑μ = x} ↔ IsCompact (closure S)

Prokhorov's theorem on D, both directions (Billingsley 1999, Theorems 5.1 and 5.2): a set of probability laws on D([0,T], E) is tight iff it is relatively compact for the topology of weak convergence.

theorem BGW.Skorokhod.bounded_and_modulus_of_isCompact_closure {T : ℝ} {E : Type u_1} [MetricSpace E] {A : Set (D T E)} (hT : 0 < T) (hA : IsCompact (closure A)) : (∃ (K : Set E), Bornology.IsBounded K ∧ ∀ f ∈ A, ∀ (t : ↑(Set.Icc 0 T)), f t ∈ K) ∧ ∀ ε > 0, ∃ (δ : ℝ), 0 < δ ∧ δ < T ∧ ∀ f ∈ A, cadlagModulus f δ ≤ ε

Billingsley 1999, Theorem 12.3, necessity: a relatively compact set of paths has values in a bounded set and uniformly vanishing modulus w' at thresholds below T. (Corollary of exists_isBounded_values_of_isCompact and exists_uniform_cadlagModulus_of_isCompact applied to closure A, monotonicity of f ↦ cadlagModulus f δ not needed.)

theorem BGW.Skorokhod.isCompact_closure_iff_bounded_and_modulus {T : ℝ} {E : Type u_1} [MetricSpace E] [ProperSpace E] {A : Set (D T E)} (hT : 0 < T) : IsCompact (closure A) ↔ (∃ (K : Set E), Bornology.IsBounded K ∧ ∀ f ∈ A, ∀ (t : ↑(Set.Icc 0 T)), f t ∈ K) ∧ ∀ ε > 0, ∃ (δ : ℝ), 0 < δ ∧ δ < T ∧ ∀ f ∈ A, cadlagModulus f δ ≤ ε

Billingsley 1999, Theorem 12.3 (iff): A ⊆ D([0,T], E), E proper, is relatively compact iff its values are bounded and lim_{δ→0} sup_{f ∈ A} w'_f(δ) = 0.

theorem BGW.Skorokhod.isTightMeasureSet_range_iff_limsup {T : ℝ} {E : Type u_1} [MetricSpace E] [ProperSpace E] (hT : 0 < T) (P : ℕ → MeasureTheory.ProbabilityMeasure (D T E)) : MeasureTheory.IsTightMeasureSet (Set.range fun (n : ℕ) => ↑(P n)) ↔ (∀ η > 0, ∃ (K : Set E), Bornology.IsBounded K ∧ Filter.limsup (fun (n : ℕ) => ↑(P n) {f : D T E | ∃ (t : ↑(Set.Icc 0 T)), f t ∉ K}) Filter.atTop ≤ ENNReal.ofReal η) ∧ ∀ ε > 0, ∀ η > 0, ∃ (δ : ℝ), 0 < δ ∧ δ < T ∧ Filter.limsup (fun (n : ℕ) => ↑(P n) {f : D T E | ε < cadlagModulus f δ}) Filter.atTop ≤ ENNReal.ofReal η

Billingsley 1999, Theorem 13.2 (iff, limsup form): a sequence of probability laws on D([0,T], E), E proper (so D is Polish and each single law is tight), is tight iff (i) for each η > 0 there is a bounded K ⊆ E with limsup_n P_n(∃ t, f t ∉ K) ≤ η (the form of lim_{a→∞} limsup_n P_n(‖f‖ ≥ a) = 0 for a general metric E), and (ii) for all ε, η > 0 there is δ ∈ (0,T) with limsup_n P_n(w'_f(δ) > ε) ≤ η (equivalent to lim_{δ→0} limsup_n P_n(w'_f(δ) ≥ ε) = 0, since w' is monotone in δ).