Predictability of left-continuous adapted nonnegative processes.

See Bertoin, Lévy Processes, Chapter IV, and Kallenberg, Foundations of Modern Probability, Chapters 12 and 22.

theorem BGW.StableTrees.measurable_predictable_of_leftContinuous {H : NNReal → Skorokhod.DLoc → ENNReal} (hadapted : ∀ (x : NNReal), Measurable (H x)) (hleft : ∀ (f : Skorokhod.DLoc) (x : NNReal), 0 < x → ContinuousWithinAt (fun (y : NNReal) => H y f) (Set.Iio x) x) : Measurable fun (p : NNReal × Skorokhod.DLoc) => H p.1 p.2

A left-continuous process adapted to the stopped filtration is predictable.