Regularity of the stable scale series

Compact majorants justify continuity and termwise differentiation.

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

theorem BGW.StableTrees.continuousOn_stableSeries {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (q : ℝ) : ContinuousOn (stableSeries θ q) (Set.Ici 0)

Continuity up to the singular derivative endpoint.

theorem BGW.StableTrees.hasDerivAt_stableSeries {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (q : ℝ) {x : ℝ} (hx : 0 < x) : HasDerivAt (stableSeries θ q) (stableSeriesDeriv θ q x) x

Termwise differentiation on (0,∞).

theorem BGW.StableTrees.continuousOn_stableSeriesDeriv {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (q : ℝ) : ContinuousOn (stableSeriesDeriv θ q) (Set.Ioi 0)

The derivative series is continuous away from its singular endpoint.

theorem BGW.StableTrees.continuous_stableSeries {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (q : ℝ) : Continuous (stableSeries θ q)

The scale series is continuous on the whole real line, with its zero extension.