Successive exits are optional times

Strict exits have a countable characterization by rational evaluations. Together with adapted evaluation at optional times, this proves the optional-time property for every finite stage of the successive-exit construction.

theorem BGW.Skorokhod.IsOptionalTime.aldousExitTime {T : ℝ} {Ω : Type u_1} {m : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration (↑(Set.Icc 0 T)) m} {σ : Ω → ↑(Set.Icc 0 T)} (hσ : IsOptionalTime 𝓕 σ) (X : Ω → D T ℝ) (hadapted : ∀ (t : ↑(Set.Icc 0 T)), Measurable fun (ω : Ω) => (X ω) t) (ε : ℝ) : IsOptionalTime 𝓕 fun (ω : Ω) => Skorokhod.aldousExitTime (X ω) ε (σ ω)

The next strict exit after an optional time is optional for every adapted càdlàg process.

Reference: Billingsley 1999, Section 16.

theorem BGW.Skorokhod.isOptionalTime_aldousExitTimes {T : ℝ} {Ω : Type u_1} {m : MeasurableSpace Ω} (hT : 0 ≤ T) (𝓕 : MeasureTheory.Filtration (↑(Set.Icc 0 T)) m) (X : Ω → D T ℝ) (hadapted : ∀ (t : ↑(Set.Icc 0 T)), Measurable fun (ω : Ω) => (X ω) t) (ε : ℝ) (k : ℕ) : IsOptionalTime 𝓕 fun (ω : Ω) => aldousExitTimes hT (X ω) ε k

Every finite stage of the successive-exit construction is an optional time.

Reference: Billingsley 1999, Section 16.