Control of the terminal window #
A strict exit after the left endpoint of the terminal window detects any large oscillation there, including a terminal jump. The nearby-optional-times estimate then supplies the endpoint control needed for merging a short final block.
theorem
BGW.Skorokhod.measure_aldous_terminal_oscillation_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)
(hadapted : ∀ (t : ↑(Set.Icc 0 T)), Measurable fun (ω : Ω) => (X ω) t)
(a : ↑(Set.Icc 0 T))
{ε δ : ℝ}
{η : ENNReal}
(hε : 0 < ε)
(hδ : 0 < δ)
(hwindow : T - ↑a ≤ δ)
(hbound :
∀ (ρ : Ω → ↑(Set.Icc 0 T)),
IsOptionalTime 𝓕 ρ →
∀ (u : ℝ), 0 ≤ u → u ≤ 2 * δ → P {ω : Ω | ε / 3 < |(X ω) (Set.projIcc 0 T hT (↑(ρ ω) + u)) - (X ω) (ρ ω)|} ≤ η)
:
Uniform Aldous increment bounds control oscillation in a deterministic terminal window.
Reference: Billingsley 1999, Section 16.