Laplace integrals for the stable scale series

Gamma integrals and absolute summability justify termwise integration.

Reference: A. E. Kyprianou, Fluctuations of Lévy Processes with Applications, 2nd ed., Springer, 2014, Chapter 8.

theorem BGW.StableTrees.integral_exp_neg_mul_normalized_rpow {a lam : ℝ} (ha : 0 < a) (hlam : 0 < lam) : MeasureTheory.IntegrableOn (fun (x : ℝ) => Real.exp (-lam * x) * x ^ (a - 1) / Real.Gamma a) (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (x : ℝ) in Set.Ioi 0, Real.exp (-lam * x) * x ^ (a - 1) / Real.Gamma a = (1 / lam) ^ a

The normalized Gamma density has Laplace integral λ⁻ᵃ on the positive half-line.

theorem BGW.StableTrees.integral_exp_neg_mul_stableSeries {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) {lam : ℝ} (hlam : q ^ (1 / θ) < lam) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (-lam * x) * stableSeries θ q x) (MeasureTheory.volume.restrict (Set.Ioi 0)) ∧ MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (-lam * x) * stableSeriesDeriv θ q x) (MeasureTheory.volume.restrict (Set.Ioi 0)) ∧ ∫ (x : ℝ) in Set.Ioi 0, Real.exp (-lam * x) * stableSeries θ q x = 1 / (lam ^ θ - q)

The tilted scale series and its derivative are integrable, with geometric Laplace sum.

theorem BGW.StableTrees.integral_exp_neg_mul_stableSeriesDeriv_sub {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) {lam : ℝ} (hlam : q ^ (1 / θ) < lam) : ∫ (x : ℝ) in Set.Ioi 0, Real.exp (-lam * x) * (stableSeriesDeriv θ q x - q ^ (1 / θ) * stableSeries θ q x) = (lam - q ^ (1 / θ)) / (lam ^ θ - q)

Transform of W_q' - Φ W_q: (λ-Φ)/(λ^θ-q) = (Φ/q) F_q(λ).