The full excursion Laplace functional, obtained by finite-box simple approximation.

See Bertoin, Lévy Processes, Chapter IV.

theorem BGW.StableTrees.excursion_laplaceFunctional {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ξ : Skorokhod.DLoc → MeasureTheory.Measure (NNReal × Excursion)} (hξ : Measurable ξ) (hae : ξ =ᵐ[↑(stableLocalLaw θ)] excursionPointMeasure) {g : NNReal × Excursion → ENNReal} (hg : Measurable g) : ∫⁻ (f : Skorokhod.DLoc), expNeg (∫⁻ (p : NNReal × Excursion), g p ∂ξ f) ∂↑(stableLocalLaw θ) = expNeg (∫⁻ (p : NNReal × Excursion), 1 - expNeg (g p) ∂lebNN.prod (excursionMeasure θ))

Laplace functional of the point measure, for every measurable ℝ≥0∞-valued test g (Campbell formula; exp (-∞) = 0 on both sides): E exp (-∫ g dξ) = exp (-∫ (1 - exp (-g)) d(Leb ⊗ N)).