Positivity and endpoint support of the normalized excursion laws

References

• 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.ae_tailExcursionLaw_support {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (e : Excursion) ∂↑(tailExcursionLaw θ), 1 < e.lifetime ∧ (∀ (t : NNReal), 0 < t → t < e.lifetime → 0 < ↑e.path t) ∧ e.lifetime = sSup {t : NNReal | 0 < ↑e.path t} ∧ Function.leftLim (↑e.path) e.lifetime = 0

Tail support: under N(· | ζ > 1), almost surely the lifetime exceeds 1, the path is positive on (0, ζ), the tag is the actual lifetime and the terminal left limit is 0.

theorem BGW.StableTrees.ae_unitExcursionLaw_positive {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (e : Excursion) ∂↑(unitExcursionLaw θ), ↑e.path 0 = 0 ∧ (∀ (t : NNReal), 0 < t → t < 1 → 0 < ↑e.path t) ∧ Function.leftLim (↑e.path) 1 = 0

Endpoints and positivity at the level of Excursion: the same properties for unitExcursionLaw, in terms of the path on ℝ≥0.