Almost-everywhere measurability of the auxiliary ladder

A countable rational crossing inverse is measurable on every path. Monotonicity identifies it with the raw inverse almost surely. This proves fixed-level a.e. measurability only, without any all-path inverse or stopping-time identification.

References

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

theorem BGW.StableTrees.aemeasurable_supAuxLadder {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (z : NNReal) : AEMeasurable (supAuxLadderTime θ z) ↑(stableLocalLaw θ) ∧ AEMeasurable (supAuxLadderHeight θ z) ↑(stableLocalLaw θ)

The inverse at each fixed level is a.e.-measurable (everywhere measurability of the totalized inverse is not claimed here).