Lifetime law, normalization and scaling of the excursion measure

For the spectrally positive θ-stable process (1 < θ ≤ 2) reflected at its infimum, with Itô excursion measure N = excursionMeasure θ and α = 1/θ:

• lintegral_one_sub_exp_lifetime: ∫ (1 - e^{-qζ}) dN = q^α (Laplace exponent of the passage subordinator);
• excursionMeasure_lifetime_tail: N(ζ > t) = t^{-α} / Γ(1 - α);
• excursionMeasure_lifetime_density: the lifetime image of N has density α / Γ(1 - α) · t^{-1-α};
• stableDensity_zero_eq_inv_theta_gamma: the stable density at 0 equals α / Γ(1 - α);
• map_excursionScale_excursionMeasure: (S_c)_* N = c^α • N.

References

• J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapters IV and VIII.
• A. E. Kyprianou, Fluctuations of Lévy Processes with Applications, 2nd ed., Springer, 2014, Chapters 6 and 8.

theorem BGW.StableTrees.stableDensity_zero_eq_inv_theta_gamma {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : Scalar.stableDensity θ 0 = 1 / (θ * Real.Gamma (1 - 1 / θ))

Normalization bridge: d_θ(0) = 1 / (θ Γ(1 - 1/θ)) (the coefficient α/Γ(1-α) of the Lévy density equals the stable density at 0).