Compactness and tightness in Skorokhod space

The oscillation uses half-open partition blocks, excluding the terminal value. The modulus tends to zero for every càdlàg path, by the finite small-oscillation partition lemma.

Uniform modulus bounds and bounded values give compact closure. The proof uses finite discretization in Billingsley's complete metric, then transfers through the identity homeomorphism. Countable error budgets give uniform tightness; the eventual form uses uniform modulus and value bounds on compact sets to include finitely many initial laws.

References: P. Billingsley, Convergence of Probability Measures, 2nd ed., 1999, §12 (the modulus w', (12.6)–(12.7), Theorem 12.3) and Theorem 13.2.

noncomputable def BGW.Skorokhod.cadlagModulus {T : ℝ} {E : Type u_1} [PseudoMetricSpace E] (f : D T E) (δ : ℝ) : ℝ

Billingsley's càdlàg modulus w'_f(δ): the infimum, over partitions 0 = t₀ < t₁ < ⋯ < t_r = T whose steps all exceed δ, of the largest oscillation of f on the half-open blocks [t_{i-1}, t_i). (It is 0 by convention when no such partition exists, e.g. for δ ≥ T; only small δ matter.)

Equations

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

theorem BGW.Skorokhod.cadlagModulus_nonneg {T : ℝ} {E : Type u_1} [PseudoMetricSpace E] (f : D T E) (δ : ℝ) : 0 ≤ cadlagModulus f δ

The modulus is nonnegative, including when the partition type is empty.

theorem BGW.Skorokhod.cadlagModulus_le_of_partition {T : ℝ} {E : Type u_1} [PseudoMetricSpace E] (f : D T E) {δ ε : ℝ} (hε : 0 ≤ ε) {r : ℕ} (t : Fin (r + 1) → ℝ) (ht0 : t 0 = 0) (htr : t (Fin.last r) = T) (hmono : StrictMono t) (hstep : ∀ (i : Fin r), δ < t i.succ - t i.castSucc) (hosc : ∀ (i : Fin r) (s u : ↑(Set.Icc 0 T)), t i.castSucc ≤ ↑s → ↑s < t i.succ → t i.castSucc ≤ ↑u → ↑u < t i.succ → dist (f s) (f u) ≤ ε) : cadlagModulus f δ ≤ ε

A partition with blocks of oscillation at most ε bounds the modulus at every smaller mesh threshold.

theorem BGW.Skorokhod.exists_partition_of_cadlagModulus_lt {T : ℝ} {E : Type u_1} [PseudoMetricSpace E] (f : D T E) {δ ε : ℝ} (hδ : 0 < δ) (hδT : δ < T) (hmod : cadlagModulus f δ < ε) : ∃ (r : ℕ) (t : Fin (r + 1) → ℝ), t 0 = 0 ∧ t (Fin.last r) = T ∧ StrictMono t ∧ (∀ (i : Fin r), δ < t i.succ - t i.castSucc) ∧ ∀ (i : Fin r) (s u : ↑(Set.Icc 0 T)), t i.castSucc ≤ ↑s → ↑s < t i.succ → t i.castSucc ≤ ↑u → ↑u < t i.succ → dist (f s) (f u) < ε

A strict modulus bound yields an actual admissible partition with the same strict oscillation bound. The infimum need not be attained.

theorem BGW.Skorokhod.cadlagModulus_eq_zero_of_nonpos {T : ℝ} {E : Type u_1} [PseudoMetricSpace E] (f : D T E) (hT : T ≤ 0) (δ : ℝ) : cadlagModulus f δ = 0

At a nonpositive time horizon the modulus is identically zero.

theorem BGW.Skorokhod.tendsto_cadlagModulus {T : ℝ} {E : Type u_1} [MetricSpace E] (f : D T E) : Filter.Tendsto (fun (δ : ℝ) => cadlagModulus f δ) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Every càdlàg path has w'_f(δ) → 0 as δ ↓ 0 (Billingsley 1999, (12.7)).

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

Arzelà–Ascoli criterion in D (sufficiency, Billingsley 1999, Theorem 12.3): a set of paths with values in a fixed bounded set of a proper space and with uniformly vanishing modulus w' has compact closure.

theorem BGW.Skorokhod.isTightMeasureSet_of_cadlagModulus {T : ℝ} {E : Type u_1} [MetricSpace E] [ProperSpace E] [MeasurableSpace (D T E)] {ι : Type u_2} (P : ι → MeasureTheory.Measure (D T E)) (hbdd : ∀ η > 0, ∃ (K : Set E), Bornology.IsBounded K ∧ ∀ (i : ι), (P i) {f : D T E | ∃ (t : ↑(Set.Icc 0 T)), f t ∉ K} ≤ ENNReal.ofReal η) (hmod : ∀ ε > 0, ∀ η > 0, ∃ (δ : ℝ), 0 < δ ∧ δ < T ∧ ∀ (i : ι), (P i) {f : D T E | ε < cadlagModulus f δ} ≤ ENNReal.ofReal η) : MeasureTheory.IsTightMeasureSet (Set.range P)

Tightness criterion in D (sufficiency, uniform form of Billingsley 1999, Theorem 13.2): if, uniformly in n, the paths stay in a bounded set with high probability and the modulus w' is small with high probability, then the laws are tight. Measures of possibly non-measurable sets are outer measures, so no measurability of w' is assumed.

theorem BGW.Skorokhod.cadlagModulus_mono {T : ℝ} {E : Type u_1} [PseudoMetricSpace E] (f : D T E) {δ d : ℝ} (hδd : δ ≤ d) (hd : 0 < d) (hdT : d < T) : cadlagModulus f δ ≤ cadlagModulus f d

The modulus increases with its threshold as long as the larger threshold admits partitions. This restriction excludes the empty-infimum convention.

theorem BGW.Skorokhod.exists_uniform_cadlagModulus_of_isCompact {T : ℝ} {E : Type u_1} [MetricSpace E] {A : Set (D T E)} (hA : IsCompact A) (hT : 0 < T) {ε : ℝ} (hε : 0 < ε) : ∃ (d : ℝ), 0 < d ∧ d < T ∧ ∀ f ∈ A, cadlagModulus f d ≤ ε

On a compact set of càdlàg paths, the moduli vanish uniformly at small positive thresholds strictly below a positive horizon.

theorem BGW.Skorokhod.exists_isBounded_values_of_isCompact {T : ℝ} {E : Type u_1} [MetricSpace E] {A : Set (D T E)} (hA : IsCompact A) : ∃ (K : Set E), Bornology.IsBounded K ∧ ∀ f ∈ A, ∀ (t : ↑(Set.Icc 0 T)), f t ∈ K

The values of all paths in a compact set lie in a single bounded subset of the state space.

theorem BGW.Skorokhod.isTightMeasureSet_of_cadlagModulus_eventually {T : ℝ} {E : Type u_1} [MetricSpace E] [ProperSpace E] [MeasurableSpace (D T E)] (P : ℕ → MeasureTheory.Measure (D T E)) (htight : ∀ (n : ℕ), MeasureTheory.IsTightMeasureSet {P n}) (hbdd : ∀ η > 0, ∃ (K : Set E), Bornology.IsBounded K ∧ ∃ (N : ℕ), ∀ n ≥ N, (P n) {f : D T E | ∃ (t : ↑(Set.Icc 0 T)), f t ∉ K} ≤ ENNReal.ofReal η) (hmod : ∀ ε > 0, ∀ η > 0, ∃ (δ : ℝ), 0 < δ ∧ δ < T ∧ ∃ (N : ℕ), ∀ n ≥ N, (P n) {f : D T E | ε < cadlagModulus f δ} ≤ ENNReal.ofReal η) : MeasureTheory.IsTightMeasureSet (Set.range P)

Tightness criterion in D in Billingsley's eventual form (Theorem 13.2, sufficiency): the bounds are only required for large n, and each single law is assumed tight (for example the law of a step path, a continuous image of a law on ℝⁿ).