Unit excursion law, lifetime/shape identity, path mixture and endpoint support

Main results:

• unitExcursionLaw, tailExcursionLaw: the unit and tail excursion laws, and levyExcLaw, tailLevyExcLaw their images as laws on Skorokhod space.
• excursionAt: the family of scaled unit excursions, with exact scaling (map_excursionScale_excursionAt).
• shapeLifetime_map_excursionMeasure: under the excursion measure, lifetime and normalized shape form a product.
• excursionMeasure_eq_lifetime_mixture, lintegral_excursionMeasure_eq_mixture: the excursion measure is the mixture of the scaled unit excursions over the lifetime.
• excursionMeasure_unique_of_scaling: uniqueness of the excursion measure from scaling.
• levyExcLaw_endpoints_pos and its Excursion-level version: endpoint and positivity statements.

References

• J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VIII.
• T. Duquesne and J.-F. Le Gall, Random Trees, Lévy Processes and Spatial Branching Processes, Astérisque 281 (2002).
• L. Chaumont, Excursion normalisée, méandre et pont pour les processus de Lévy stables, Bull. Sci. Math. 121 (1997), 377–403.

theorem BGW.StableTrees.levyExcLaw_endpoints_pos {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (x : Skorokhod.D 1 ℝ) ∂↑(levyExcLaw θ), x ⟨0, ⋯⟩ = 0 ∧ (∀ (t : ↑(Set.Icc 0 1)), 0 < ↑t → ↑t < 1 → 0 < x t) ∧ x ⟨1, ⋯⟩ = 0 ∧ Function.leftLim ⇑x ⟨1, ⋯⟩ = 0

Endpoints and positivity for the unit excursion: almost surely e 0 = 0, e t > 0 on (0,1), e 1 = 0 and the left limit at 1 is 0.