Identification of the lifetime image measure by its finite positive tails.

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

theorem BGW.StableTrees.excursionMeasure_lifetime_density {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : MeasureTheory.Measure.map Excursion.lifetime (excursionMeasure θ) = lebNN.withDensity fun (t : NNReal) => ENNReal.ofReal (1 / θ / Real.Gamma (1 - 1 / θ) * ↑t ^ (-1 - 1 / θ))

Lifetime density: the image of N under the lifetime is (1/θ)/Γ(1-1/θ) · t^{-1-1/θ} dt on (0,∞) (Lévy measure of the passage subordinator).