Measurability of the marked excursion measure

Rational physical times enumerate all passage-jump labels through local time. Keeping the first occurrence of each label yields a measurable sum of Dirac masses.

(J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV, Sections 2–4; K. Itô, Poisson point processes attached to Markov processes, Proc. Sixth Berkeley Symp. Math. Statist. Probab. 3 (1972), 225–239.)

theorem BGW.StableTrees.aemeasurable_excursionPointMeasure {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : AEMeasurable excursionPointMeasure ↑(stableLocalLaw θ)

Random-measure measurability: the map f ↦ excursionPointMeasure f is AEMeasurable (into Measure (ℝ≥0 × Excursion) with its Giry/evaluation σ-algebra).

theorem BGW.StableTrees.exists_measurable_modification_excursionPointMeasure {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∃ (ξ : Skorokhod.DLoc → MeasureTheory.Measure (NNReal × Excursion)), Measurable ξ ∧ ξ =ᵐ[↑(stableLocalLaw θ)] excursionPointMeasure

Measurable modification (the measurable field of IsTimeSimpleLevy): there is a measurable map ξ : DLoc → Measure (ℝ≥0 × Excursion) a.s. equal to excursionPointMeasure.

theorem BGW.StableTrees.aemeasurable_excursionPointMeasure_apply {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {s : Set (NNReal × Excursion)} (hs : MeasurableSet s) : AEMeasurable (fun (f : Skorokhod.DLoc) => (excursionPointMeasure f) s) ↑(stableLocalLaw θ)

Box counts are AE-measurable (all measurable boxes/sets).

theorem BGW.StableTrees.exists_stopped_measurable_restrict_Iic {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : NNReal) : ∃ (G : Skorokhod.DLoc → MeasureTheory.Measure (NNReal × Excursion)), Measurable G ∧ (fun (f : Skorokhod.DLoc) => (excursionPointMeasure f).restrict (Set.Iic a ×ˢ Set.univ)) =ᵐ[↑(stableLocalLaw θ)] G

Past labels are F_{T_a}-measurable (up to a null set): the restriction of μ to labels ≤ a agrees a.s. with an F_{T_a}-measurable random measure (all those excursions end by T_a).