Absolute continuity of the stable scale series

Nonnegative derivatives give integrability at zero. The series at |q| dominates signed rates, and the fundamental theorem of calculus identifies the integral.

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

theorem BGW.StableTrees.measurable_stableSeriesDeriv {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (q : ℝ) : Measurable (stableSeriesDeriv θ q)

The termwise derivative is Borel, including its specified value at zero.

theorem BGW.StableTrees.stableSeriesDeriv_nonneg {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 ≤ q) (x : ℝ) : 0 ≤ stableSeriesDeriv θ q x

The derivative series is nonnegative at nonnegative rates.

theorem BGW.StableTrees.norm_stableSeriesDeriv_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (q x : ℝ) : ‖stableSeriesDeriv θ q x‖ ≤ stableSeriesDeriv θ |q| x

Absolute derivative bounds for signed rates follow from the positive-rate series.

theorem BGW.StableTrees.integrableOn_stableSeriesDeriv {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (q K : ℝ) : MeasureTheory.IntegrableOn (stableSeriesDeriv θ q) (Set.Ioc 0 K) MeasureTheory.volume

Local integrability of W_q' at 0 (integrable singularity x^{θ-2} for θ < 2).

theorem BGW.StableTrees.integral_stableSeriesDeriv {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (q : ℝ) {x : ℝ} (hx : 0 ≤ x) : ∫ (y : ℝ) in Set.Ioc 0 x, stableSeriesDeriv θ q y = stableSeries θ q x

W_q(x) = ∫_0^x W_q' (absolute continuity at the singular endpoint 0).