Convergence and differentiation of the stable scale series

Gamma monotonicity gives factorial majorants for every compact interval.

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

theorem BGW.StableTrees.summable_stableSeriesTerm {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (q : ℝ) {x : ℝ} (hx : 0 ≤ x) : Summable fun (n : ℕ) => stableSeriesTerm θ q n x

Absolute convergence of the stable scale series at nonnegative arguments.

theorem BGW.StableTrees.summable_stableSeriesDerivTerm {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (q : ℝ) {x : ℝ} (hx : 0 < x) : Summable fun (n : ℕ) => stableSeriesDerivTerm θ q n x

Absolute convergence of the termwise derivative away from the endpoint.