Documentation

BGW.StableTrees.SupremumPotentialZeroRate

Uniform zero-rate limit of the stable scale series #

A compact majorant makes the series jointly continuous in its rate and argument.

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

theorem BGW.StableTrees.continuousOn_stableSeries_rate_argument {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (K : ℝ) :
ContinuousOn (fun (p : ℝ × ℝ) => stableSeries θ p.1 p.2) (Set.Icc 0 1 ×ˢ Set.Icc 0 K)

Joint continuity of the rate and spatial argument on compact positive rectangles.

theorem BGW.StableTrees.tendstoUniformlyOn_stableSeries_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (K : ℝ) :
TendstoUniformlyOn (fun (q x : ℝ) => stableSeries θ q x) (stableScale θ) (nhdsWithin 0 (Set.Ioi 0)) (Set.Icc 0 K)

The scale series tends locally uniformly to the zero-rate scale.