Counting short exit gaps #
Among sufficiently many successive gaps in a bounded horizon, at least half are short. A finite counting argument turns uniform probability bounds for individual short gaps into a bound for the event that many exits occur.
theorem
BGW.Skorokhod.measure_aldousExitTimes_lt_terminal_le
{T : ℝ}
{Ω : Type u_1}
[m : MeasurableSpace Ω]
(hT : 0 ≤ T)
(P : MeasureTheory.Measure Ω)
(𝓕 : MeasureTheory.Filtration (↑(Set.Icc 0 T)) m)
(X : Ω → D T ℝ)
(hadapted : ∀ (t : ↑(Set.Icc 0 T)), Measurable fun (ω : Ω) => (X ω) t)
(ε : ℝ)
{δ : ℝ}
{η : ENNReal}
(hδ : 0 < δ)
{K : ℕ}
(hK : 2 * T < ↑K * δ)
(hgap :
∀ (k : ℕ),
P
{ω : Ω | ↑(aldousExitTimes hT (X ω) ε (k + 1)) < T ∧ ↑(aldousExitTimes hT (X ω) ε (k + 1)) - ↑(aldousExitTimes hT (X ω) ε k) ≤ δ} ≤ η)
:
Uniform bounds on individual genuine short gaps bound the tail of the number of exits.
Reference: Billingsley 1999, Section 16.