Power-law lifetime tails from scaling and the unit Laplace exponent.

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapters IV and VIII.

theorem BGW.StableTrees.excursionMeasure_lifetime_tail_scale {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : ℝ) (ht : 0 < t) : (excursionMeasure θ) {e : Excursion | t < ↑e.lifetime} = ENNReal.ofReal (t ^ (-(1 / θ))) * (excursionMeasure θ) {e : Excursion | 1 < ↑e.lifetime}

Scaling determines every positive lifetime tail from its value at one.

theorem BGW.StableTrees.excursionMeasure_lifetime_tail {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : ℝ) (ht : 0 < t) : (excursionMeasure θ) {e : Excursion | t < ↑e.lifetime} = ENNReal.ofReal (t ^ (-(1 / θ)) / Real.Gamma (1 - 1 / θ))

Lifetime tail: N(ζ > t) = t^{-1/θ} / Γ(1 - 1/θ) for t > 0.