Tightness from probability bounds on source spaces

The random variables can live on different probability spaces. Bounds are imposed directly on source events. This avoids any measurability assumption for the càdlàg modulus: the final compact set is closed and hence Borel measurable.

theorem BGW.Skorokhod.isTightMeasureSet_of_source_cadlagModulus_eventually {T : ℝ} {Ω : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (Ω n)] (P : (n : ℕ) → MeasureTheory.Measure (Ω n)) (X : (n : ℕ) → Ω n → D T ℝ) (hX : ∀ (n : ℕ), Measurable (X n)) (htight : ∀ (n : ℕ), MeasureTheory.IsTightMeasureSet {MeasureTheory.Measure.map (X n) (P n)}) (hbdd : ∀ η > 0, ∃ (K : Set ℝ), Bornology.IsBounded K ∧ ∃ (N : ℕ), ∀ n ≥ N, (P n) {ω : Ω n | ∃ (t : ↑(Set.Icc 0 T)), (X n ω) t ∉ K} ≤ ENNReal.ofReal η) (hmod : ∀ ε > 0, ∀ η > 0, ∃ (δ : ℝ), 0 < δ ∧ δ < T ∧ ∃ (N : ℕ), ∀ n ≥ N, (P n) {ω : Ω n | ε < cadlagModulus (X n ω) δ} ≤ ENNReal.ofReal η) : MeasureTheory.IsTightMeasureSet (Set.range fun (n : ℕ) => MeasureTheory.Measure.map (X n) (P n))

Eventual source-space estimates suffice when the finitely many initial laws are tight.

Reference: Billingsley 1999, Section 16.