Merging the terminal block of an exit partition #
Only genuine exits need to be well separated. If the terminal sentinel is too close to the last exit, merge the last two blocks. Control of the oscillation in a deterministic terminal window bounds the resulting block.
theorem
BGW.Skorokhod.cadlagModulus_le_of_aldous_gaps
{T : ℝ}
(hT : 0 < T)
(f : D T ℝ)
{ε δ : ℝ}
(hε : 0 ≤ ε)
(hδ : 0 < δ)
(hδT : 4 * δ < T)
(K : ℕ)
(hstop : ↑(aldousExitTimes ⋯ f ε K) = T)
(hgap :
∀ j < K, ↑(aldousExitTimes ⋯ f ε (j + 1)) < T → 2 * δ < ↑(aldousExitTimes ⋯ f ε (j + 1)) - ↑(aldousExitTimes ⋯ f ε j))
(hterm : ∀ (t : ↑(Set.Icc 0 T)), T - 2 * δ ≤ ↑t → |f t - f ⟨T - 2 * δ, ⋯⟩| ≤ ε)
:
Genuine exit gaps suffice for a modulus bound once the terminal window is controlled.
Reference: Billingsley 1999, Section 16.