Jump times as stopping times

The first jump after a rational time with size above a positive rational threshold is a stopping time for the right-continuous filtration on DLoc. Enumerating the rational parameters therefore gives a countable family of stopping times containing every jump time of every path (the bounded-horizon version of the jump-time argument of P. W. Millar, Zero-one laws and the minimum of a Markov process, Trans. Amer. Math. Soc. 226 (1977), 365–391).

theorem BGW.Skorokhod.isStoppingTime_firstJumpAbove (q : ℚ≥0) {ε : ℚ} (hε : 0 < ε) : MeasureTheory.IsStoppingTime DLoc.filtration fun (f : DLoc) => firstJumpAbove ↑q ↑ε ↑f

The time σ_{q,ε} is a stopping time of the right-continuous filtration, for rational q ≥ 0 and rational ε > 0 (formulated on DLoc paths, as a WithTop ℝ≥0-valued time).

theorem BGW.Skorokhod.exists_jumpStoppingTimes : ∃ (J : ℕ → DLoc → WithTop NNReal), (∀ (n : ℕ), MeasureTheory.IsStoppingTime DLoc.filtration (J n)) ∧ ∀ (f : DLoc) (t : NNReal), 0 < t → ↑f t ≠ Function.leftLim (↑f) t → ∃ (n : ℕ), J n f = ↑t

Jump enumeration. There are countably many stopping times of DLoc.filtration such that every path's every jump time t > 0 is one of them.