Identification of the mean excursion point measure with the product intensity.

See Bertoin, Lévy Processes, Chapter IV.

theorem BGW.StableTrees.lebNN_singleton_zero : lebNN {0} = 0

The local-time Lebesgue measure has no mass at the origin.

theorem BGW.StableTrees.lebNN_Iic (a : NNReal) : lebNN (Set.Iic a) = ↑a

The local-time Lebesgue measure of an initial closed interval.

theorem BGW.StableTrees.sigmaFinite_lebNN : MeasureTheory.SigmaFinite lebNN

The local-time Lebesgue measure is sigma finite.

theorem BGW.StableTrees.lintegral_pointMeasure_eq_prod {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ξ : Skorokhod.DLoc → MeasureTheory.Measure (NNReal × Excursion)} (hξ : Measurable ξ) (hae : ξ =ᵐ[↑(stableLocalLaw θ)] excursionPointMeasure) {B : Set (NNReal × Excursion)} (hB : MeasurableSet B) : ∫⁻ (f : Skorokhod.DLoc), (ξ f) B ∂↑(stableLocalLaw θ) = (lebNN.prod (excursionMeasure θ)) B

Intensity measure is Leb ⊗ N: E ξ(B) = (lebNN.prod N)(B) for measurable B.