Exponential transforms of finite disjoint measurable partitions inside finite-rate boxes.

See Bertoin, Lévy Processes, Chapter IV.

theorem BGW.StableTrees.excursion_laplace_partition {ι : Type u_1} [Fintype ι] {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ξ : Skorokhod.DLoc → MeasureTheory.Measure (NNReal × Excursion)} (hξ : Measurable ξ) (hae : ξ =ᵐ[↑(stableLocalLaw θ)] excursionPointMeasure) (T ε : NNReal) (hε : 0 < ε) (B : ι → Set (NNReal × Excursion)) (hB : ∀ (i : ι), MeasurableSet (B i)) (hsub : ∀ (i : ι), B i ⊆ Set.Ioc 0 T ×ˢ {e : Excursion | ε < e.lifetime}) (hd : Pairwise (Function.onFun Disjoint B)) (c : ι → ENNReal) : ∫⁻ (f : Skorokhod.DLoc), expNeg (∑ i : ι, c i * (ξ f) (B i)) ∂↑(stableLocalLaw θ) = expNeg (∑ i : ι, (1 - expNeg (c i)) * (lebNN.prod (excursionMeasure θ)) (B i))

Finite disjoint measurable partitions in a lifetime-slab box have the Poisson exponential transform, including infinite coefficients.