Deterministic exit partitions for Aldous's criterion

Successive strict exits from balls of radius ε control the oscillation by 2 * ε on each half-open block. The terminal block is included in the mesh hypothesis: separation of the genuine exits alone does not ensure an admissible partition.

def BGW.Skorokhod.aldousExitSet {T : ℝ} (f : D T ℝ) (ε : ℝ) (s : ↑(Set.Icc 0 T)) : Set ℝ

Times of strict exits from the ball about f s, together with the terminal sentinel.

Reference: Billingsley 1999, Section 16.

Equations

• BGW.Skorokhod.aldousExitSet f ε s = insert T (Subtype.val '' {u : ↑(Set.Icc 0 T) | s < u ∧ ε < |f u - f s|})

theorem BGW.Skorokhod.aldousExitSet_nonempty {T : ℝ} (f : D T ℝ) (ε : ℝ) (s : ↑(Set.Icc 0 T)) : (aldousExitSet f ε s).Nonempty

The terminal sentinel makes the exit set nonempty.

Reference: Billingsley 1999, Section 16.

theorem BGW.Skorokhod.aldousExitSet_lower {T : ℝ} (f : D T ℝ) (ε : ℝ) (s : ↑(Set.Icc 0 T)) (u : ℝ) : u ∈ aldousExitSet f ε s → ↑s ≤ u

Every candidate exit is at or after the starting time.

Reference: Billingsley 1999, Section 16.

noncomputable def BGW.Skorokhod.aldousExitTime {T : ℝ} (f : D T ℝ) (ε : ℝ) (s : ↑(Set.Icc 0 T)) : ↑(Set.Icc 0 T)

First strict exit from the ball of radius ε about f s after s, capped at T.

Reference: Billingsley 1999, Section 16.

Equations

• BGW.Skorokhod.aldousExitTime f ε s = ⟨sInf (BGW.Skorokhod.aldousExitSet f ε s), ⋯⟩

theorem BGW.Skorokhod.le_aldousExitTime {T : ℝ} (f : D T ℝ) (ε : ℝ) (s : ↑(Set.Icc 0 T)) : s ≤ aldousExitTime f ε s

The capped next exit is no earlier than the starting time.

Reference: Billingsley 1999, Section 16.

theorem BGW.Skorokhod.abs_sub_le_before_aldousExitTime {T : ℝ} (f : D T ℝ) {ε : ℝ} {s u : ↑(Set.Icc 0 T)} (hε : 0 ≤ ε) (hsu : s ≤ u) (hu : u < aldousExitTime f ε s) : |f u - f s| ≤ ε

Before the next strict exit, the path stays within the prescribed radius.

Reference: Billingsley 1999, Section 16.

theorem BGW.Skorokhod.lt_aldousExitTime {T : ℝ} (f : D T ℝ) {ε : ℝ} (hε : 0 < ε) {s : ↑(Set.Icc 0 T)} (hs : ↑s < T) : s < aldousExitTime f ε s

Positive-radius exits strictly advance before the horizon, by right continuity.

Reference: Billingsley 1999, Section 16.

noncomputable def BGW.Skorokhod.aldousExitTimes {T : ℝ} (hT : 0 ≤ T) (f : D T ℝ) (ε : ℝ) : ℕ → ↑(Set.Icc 0 T)

Successive strict exits from balls of radius ε, with the terminal time absorbing.

Reference: Billingsley 1999, Section 16.

Equations

• BGW.Skorokhod.aldousExitTimes hT f ε 0 = ⟨0, ⋯⟩
• BGW.Skorokhod.aldousExitTimes hT f ε k.succ = BGW.Skorokhod.aldousExitTime f ε (BGW.Skorokhod.aldousExitTimes hT f ε k)

theorem BGW.Skorokhod.cadlagModulus_le_of_aldousExitTimes {T : ℝ} (hT : 0 ≤ T) (f : D T ℝ) {ε δ : ℝ} (hε : 0 ≤ ε) {K : ℕ} (hterminal : ↑(aldousExitTimes hT f ε K) = T) (hmono : StrictMono fun (i : Fin (K + 1)) => aldousExitTimes hT f ε ↑i) (hgap : ∀ (i : Fin K), δ < ↑(aldousExitTimes hT f ε ↑i.succ) - ↑(aldousExitTimes hT f ε ↑i.castSucc)) : cadlagModulus f δ ≤ 2 * ε

A finite exit partition, including its terminal gap, bounds the càdlàg modulus.

Reference: Billingsley 1999, Section 16.