Lifetime marginal and atomlessness of normalized tail 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.sigmaFinite_lifetimeLaw (θ : ℝ) : MeasureTheory.SigmaFinite (lifetimeLaw θ)

The lifetime density defines a sigma-finite measure for every index.

theorem BGW.StableTrees.map_lifetimePos_excursionMeasure {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : MeasureTheory.Measure.map Excursion.lifetimePos (excursionMeasure θ) = lifetimeLaw θ

Lifetime marginal on the positive half-line: (lifetimePos)_* N = lifetimeLaw.

theorem BGW.StableTrees.excursionMeasure_lifetime_eq_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : ℝ) (ha : 0 < a) : (excursionMeasure θ) {e : Excursion | ↑e.lifetime = a} = 0

No positive lifetime is charged by N.

theorem BGW.StableTrees.tailExcursionLaw_lifetime_eq_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : ℝ) : ↑(tailExcursionLaw θ) {e : Excursion | ↑e.lifetime = a} = 0

No lifetime is charged by the tail law.