Finiteness of successive exits

At a nonterminal exit the displacement is at least the radius. Infinitely many positive-radius exits would accumulate from the left, contradicting the left limit of the càdlàg path.

theorem BGW.Skorokhod.le_abs_sub_aldousExitTime {T : ℝ} (f : D T ℝ) (ε : ℝ) (s : ↑(Set.Icc 0 T)) (hterminal : ↑(aldousExitTime f ε s) < T) : ε ≤ |f (aldousExitTime f ε s) - f s|

At a nonterminal strict exit, the displacement is at least the exit radius.

Reference: Billingsley 1999, Section 16.

theorem BGW.Skorokhod.le_abs_sub_aldousExitTime_of_exists {T : ℝ} (f : D T ℝ) {ε : ℝ} (hε : 0 ≤ ε) (s : ↑(Set.Icc 0 T)) (hex : ∃ (u : ↑(Set.Icc 0 T)), s ≤ u ∧ ε < |f u - f s|) : ε ≤ |f (aldousExitTime f ε s) - f s|

If a strict displacement occurs, the capped exit also has a large displacement, including when the exit is at the horizon.

Reference: Billingsley 1999, Section 16.

theorem BGW.Skorokhod.monotone_aldousExitTimes {T : ℝ} (hT : 0 ≤ T) (f : D T ℝ) (ε : ℝ) : Monotone (aldousExitTimes hT f ε)

Successive capped exits form a nondecreasing sequence.

Reference: Billingsley 1999, Section 16.

theorem BGW.Skorokhod.exists_aldousExitTimes_eq_terminal {T : ℝ} (hT : 0 ≤ T) (f : D T ℝ) {ε : ℝ} (hε : 0 < ε) : ∃ (K : ℕ), ↑(aldousExitTimes hT f ε K) = T

Only finitely many positive-radius exits occur before a compact horizon.

Reference: Billingsley 1999, Section 16.