Transfer of measurable mark properties from the jump excursions to the mean mark measure.

See Bertoin, Lévy Processes, Chapter IV.

theorem BGW.StableTrees.ae_excursionMeasure_of_ae_jumpExcursion {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {Q : Excursion → Prop} (hQ : MeasurableSet {e : Excursion | Q e}) (hmarks : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ x ∈ passageJumpSet f, Q (jumpExcursion x f)) : ∀ᵐ (e : Excursion) ∂excursionMeasure θ, Q e

A measurable property shared by all jump marks almost surely holds almost everywhere for the excursion measure. The measurability hypothesis must be proved before applying this lemma to a property quantified over all times.