Probability bounds for nearby optional times #
Averaging over deterministic offsets bounds a large displacement between optional
times at distance at most δ. The estimate applies to genuine exits, where a
large displacement is present; it does not count the terminal sentinel as an exit.
theorem
BGW.Skorokhod.measure_short_aldous_pair_le
{T : ℝ}
{Ω : Type u_1}
[m : MeasurableSpace Ω]
(hT : 0 ≤ T)
(P : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure P]
(𝓕 : MeasureTheory.Filtration (↑(Set.Icc 0 T)) m)
(X : Ω → D T ℝ)
(hX : Measurable X)
(τ σ : Ω → ↑(Set.Icc 0 T))
(hτ : IsOptionalTime 𝓕 τ)
(hσ : IsOptionalTime 𝓕 σ)
{ε δ : ℝ}
{η : ENNReal}
(hδ : 0 < δ)
(hbound :
∀ (ρ : Ω → ↑(Set.Icc 0 T)),
IsOptionalTime 𝓕 ρ →
∀ (u : ℝ), 0 ≤ u → u ≤ 2 * δ → P {ω : Ω | ε < |(X ω) (Set.projIcc 0 T hT (↑(ρ ω) + u)) - (X ω) (ρ ω)|} ≤ η)
:
Uniform deterministic-offset bounds control large displacements between nearby optional times, with no independence assumption.
Reference: Billingsley 1999, Section 16.
theorem
BGW.Skorokhod.exists_uniform_aldous_exit_gap_bound
{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)
(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,
∀ (k : ℕ),
(P n)
{ω : Ω n | ↑(aldousExitTimes ⋯ (X n ω) ε (k + 1)) < T ∧ ↑(aldousExitTimes ⋯ (X n ω) ε (k + 1)) - ↑(aldousExitTimes ⋯ (X n ω) ε k) ≤ δ} ≤ 4 * ENNReal.ofReal η
Aldous's sequence condition bounds every genuine short exit gap uniformly in its index. The terminal sentinel is excluded because its gap can be arbitrarily short.
Reference: Billingsley 1999, Section 16.