Basic tools for Aldous's tightness criterion

Bounded stopping times and the diagonal argument converting the sequence condition into a bound uniform over stopping times and small deterministic time increments. The remaining modules build the exit estimates and tightness criterion from these tools.

def BGW.Skorokhod.IsStopTime {T : ℝ} {Ω : Type u_1} {m : MeasurableSpace Ω} (𝓕 : MeasureTheory.Filtration (↑(Set.Icc 0 T)) m) (τ : Ω → ↑(Set.Icc 0 T)) : Prop

τ : Ω → [0,T] is a stopping time for 𝓕.

Reference: Billingsley 1999, Section 16.

Equations

• BGW.Skorokhod.IsStopTime 𝓕 τ = ∀ (t : ↑(Set.Icc 0 T)), MeasurableSet {ω : Ω | τ ω ≤ t}

theorem BGW.Skorokhod.isStopTime_const {T : ℝ} {Ω : Type u_1} {m : MeasurableSpace Ω} (𝓕 : MeasureTheory.Filtration (↑(Set.Icc 0 T)) m) (t : ↑(Set.Icc 0 T)) : IsStopTime 𝓕 fun (x : Ω) => t

A deterministic bounded time is a stopping time.

Reference: Billingsley 1999, Section 16.

theorem BGW.Skorokhod.isStopTime_iff_isStoppingTime {T : ℝ} {Ω : Type u_1} {m : MeasurableSpace Ω} (𝓕 : MeasureTheory.Filtration (↑(Set.Icc 0 T)) m) (τ : Ω → ↑(Set.Icc 0 T)) : IsStopTime 𝓕 τ ↔ MeasureTheory.IsStoppingTime 𝓕 fun (ω : Ω) => ↑(τ ω)

Bounded stopping times agree with Mathlib's stopping times after coercion to WithTop.

Reference: Billingsley 1999, Section 16.

theorem BGW.Skorokhod.exists_uniform_aldous_bound {T : ℝ} (hT : 0 < T) {Ω : ℕ → Type u_1} [m : (n : ℕ) → MeasurableSpace (Ω n)] (P : (n : ℕ) → MeasureTheory.Measure (Ω n)) (𝓕 : (n : ℕ) → MeasureTheory.Filtration (↑(Set.Icc 0 T)) (m n)) (X : (n : ℕ) → Ω n → D T ℝ) (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)) {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) : ∃ δ > 0, ∃ (N : ℕ), ∀ n ≥ N, ∀ (τ : Ω n → ↑(Set.Icc 0 T)), IsStopTime (𝓕 n) τ → ∀ (h : ℝ), 0 ≤ h → h ≤ δ → (P n) {ω : Ω n | ε ≤ |(X n ω) (Set.projIcc 0 T ⋯ (↑(τ ω) + h)) - (X n ω) (τ ω)|} ≤ ENNReal.ofReal η

The sequence form of Aldous's condition gives an eventual bound uniform over bounded stopping times and sufficiently small nonnegative deterministic increments.

Reference: Billingsley 1999, Section 16.