Averaging bounds for short exit gaps

Displacements at two nearby random times are compared with their displacements over deterministic offsets by averaging over an interval of offsets. Translation invariance removes the random difference of the two starting times.

theorem BGW.Skorokhod.measure_le_four_mul_of_aldous_cover {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.SFinite P] {δ : ℝ} (hδ : 0 < δ) {η : ENNReal} {A B : ℝ → Ω → ENNReal} (hA : Measurable (Function.uncurry A)) (hB : Measurable (Function.uncurry B)) {E : Set Ω} (hE : MeasurableSet E) (d : Ω → ℝ) (hcover : ∀ ω ∈ E, ∀ u ∈ Set.Icc δ (2 * δ), 1 ≤ A u ω + B (u - d ω) ω) (hAbound : ∀ (u : ℝ), ∫⁻ (ω : Ω), A u ω ∂P ≤ (Set.Icc 0 (2 * δ)).indicator (fun (x : ℝ) => η) u) (hBbound : ∀ (u : ℝ), ∫⁻ (ω : Ω), B u ω ∂P ≤ (Set.Icc 0 (2 * δ)).indicator (fun (x : ℝ) => η) u) : P E ≤ 4 * η

A pointwise interval cover and uniform integral bounds yield a probability bound. The offset d can depend arbitrarily on the sample.

Reference: Billingsley 1999, Section 16.