Aldous's tightness criterion on Skorokhod space

Aldous's sequence condition and compact containment imply tightness of the path laws. The proof passes through optional strict exit times, averages deterministic offsets for the short-gap estimate, bounds the number of exits, and merges a short terminal block using endpoint control. Fixed-time tightness supplies compact containment via finitely many deterministic control times and the modulus bound.

References

• D. Aldous, Stopping times and tightness, Ann. Probab. 6 (1978), 335–340.
• P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999, Section 16.

theorem BGW.Skorokhod.isTightMeasureSet_of_aldous {T : ℝ} (hT : 0 < T) {Ω : ℕ → Type u_1} [m : (n : ℕ) → MeasurableSpace (Ω n)] (P : (n : ℕ) → MeasureTheory.Measure (Ω n)) [∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (P n)] (𝓕 : (n : ℕ) → MeasureTheory.Filtration (↑(Set.Icc 0 T)) (m n)) (X : (n : ℕ) → Ω n → D T ℝ) (hX : ∀ (n : ℕ), Measurable (X n)) (hadapted : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)), Measurable fun (ω : Ω n) => (X n ω) t) (hsup : ∀ η > 0, ∃ (c : ℝ), Filter.limsup (fun (n : ℕ) => (P n) {ω : Ω n | ∃ (t : ↑(Set.Icc 0 T)), c ≤ |(X n ω) t|}) Filter.atTop ≤ ENNReal.ofReal η) (hAldous : ∀ (τ : (n : ℕ) → Ω n → ↑(Set.Icc 0 T)), (∀ (n : ℕ), IsStopTime (𝓕 n) (τ n)) → ∀ (h : ℕ → ℝ), (∀ (n : ℕ), 0 ≤ h n) → Filter.Tendsto h Filter.atTop (nhds 0) → ∀ ε > 0, Filter.Tendsto (fun (n : ℕ) => (P n) {ω : Ω n | ε ≤ |(X n ω) (Set.projIcc 0 T ⋯ (↑(τ n ω) + h n)) - (X n ω) (τ n ω)|}) Filter.atTop (nhds 0)) : MeasureTheory.IsTightMeasureSet (Set.range fun (n : ℕ) => MeasureTheory.Measure.map (X n) (P n))

Billingsley 1999, Theorem 16.10 (sufficiency).

theorem BGW.Skorokhod.isTightMeasureSet_of_aldous_fixedTimes {T : ℝ} (hT : 0 < T) {Ω : ℕ → Type u_1} [m : (n : ℕ) → MeasurableSpace (Ω n)] (P : (n : ℕ) → MeasureTheory.Measure (Ω n)) [∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (P n)] (𝓕 : (n : ℕ) → MeasureTheory.Filtration (↑(Set.Icc 0 T)) (m n)) (X : (n : ℕ) → Ω n → D T ℝ) (hX : ∀ (n : ℕ), Measurable (X n)) (hadapted : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)), Measurable fun (ω : Ω n) => (X n ω) t) (hfixed : ∀ (t : ↑(Set.Icc 0 T)), ∀ η > 0, ∃ (c : ℝ), Filter.limsup (fun (n : ℕ) => (P n) {ω : Ω n | c ≤ |(X n ω) t|}) Filter.atTop ≤ ENNReal.ofReal η) (hAldous : ∀ (τ : (n : ℕ) → Ω n → ↑(Set.Icc 0 T)), (∀ (n : ℕ), IsStopTime (𝓕 n) (τ n)) → ∀ (h : ℕ → ℝ), (∀ (n : ℕ), 0 ≤ h n) → Filter.Tendsto h Filter.atTop (nhds 0) → ∀ ε > 0, Filter.Tendsto (fun (n : ℕ) => (P n) {ω : Ω n | ε ≤ |(X n ω) (Set.projIcc 0 T ⋯ (↑(τ n ω) + h n)) - (X n ω) (τ n ω)|}) Filter.atTop (nhds 0)) : MeasureTheory.IsTightMeasureSet (Set.range fun (n : ℕ) => MeasureTheory.Measure.map (X n) (P n))

Same conclusion with the sup-norm tightness (i) replaced by tightness of X^n_t at every fixed time t ∈ [0,T] (Billingsley 1999, Theorem 16.10 with fixed-time tightness). Tightness of X^n_0 alone is NOT enough: X^n_t = n·1{U ≤ t} with U uniform satisfies Aldous's condition and has tight X^n_0 = 0, but is not tight.