Laplace functionals of simple tests supported in a finite-rate box.

See Bertoin, Lévy Processes, Chapter IV.

theorem BGW.StableTrees.excursion_laplace_simple {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ξ : Skorokhod.DLoc → MeasureTheory.Measure (NNReal × Excursion)} (hξ : Measurable ξ) (hae : ξ =ᵐ[↑(stableLocalLaw θ)] excursionPointMeasure) (T ε : NNReal) (hε : 0 < ε) (g : MeasureTheory.SimpleFunc (NNReal × Excursion) ENNReal) (hgs : Function.support ⇑g ⊆ Set.Ioc 0 T ×ˢ {e : Excursion | ε < e.lifetime}) : ∫⁻ (f : Skorokhod.DLoc), expNeg (∫⁻ (p : NNReal × Excursion), g p ∂ξ f) ∂↑(stableLocalLaw θ) = expNeg (∫⁻ (p : NNReal × Excursion), 1 - expNeg (g p) ∂lebNN.prod (excursionMeasure θ))

The excursion Laplace functional for a simple test supported in a bounded slab box.