Fixed-time tightness and compact containment

Finite deterministic control times convert fixed-time tightness and a modulus estimate into an eventual uniform bound on all path values.

theorem BGW.Skorokhod.exists_eventual_value_bound_of_fixedTimes {T : ℝ} (hT : 0 < T) {Ω : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (Ω n)] (P : (n : ℕ) → MeasureTheory.Measure (Ω n)) (X : (n : ℕ) → Ω n → D T ℝ) (hfixed : ∀ (t : ↑(Set.Icc 0 T)), ∀ η > 0, ∃ (c : ℝ), Filter.limsup (fun (n : ℕ) => (P n) {ω : Ω n | c ≤ |(X n ω) t|}) Filter.atTop ≤ ENNReal.ofReal η) (hmod : ∀ η > 0, ∃ (δ : ℝ), 0 < δ ∧ δ < T ∧ ∃ (N : ℕ), ∀ n ≥ N, (P n) {ω : Ω n | 1 < cadlagModulus (X n ω) δ} ≤ ENNReal.ofReal η) (η : ℝ) : η > 0 → ∃ (K : Set ℝ), Bornology.IsBounded K ∧ ∃ (N : ℕ), ∀ n ≥ N, (P n) {ω : Ω n | ∃ (t : ↑(Set.Icc 0 T)), (X n ω) t ∉ K} ≤ ENNReal.ofReal η

Fixed-time tightness and a probability bound for the modulus imply compact containment.

Reference: Billingsley 1999, Section 16.