Predictable passage starts and fixed levels

Left passage times are predictable by a rational supremum of left-continuous adapted steps. The diffuse intensity of the marked excursion measure excludes jumps at fixed levels.

References

J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.

theorem BGW.StableTrees.measurable_predictable_passageTimeMinus : Measurable fun (p : NNReal × Skorokhod.DLoc) => passageTimeMinus p.1 p.2

The left passage-time process is measurable for the stopped predictable sigma algebra.

theorem BGW.StableTrees.ae_passageTimeMinus_eq_passageTime {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), passageTimeMinus x f = passageTime x f

At every fixed local-time level, the left passage time equals the passage time a.s.