Uniform convergence of occupation potentials

Uniform continuity of the extended supremum potential controls all initial states at once in the convolution formula.

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

theorem BGW.StableTrees.tendstoUniformlyOn_supOccupationResolvent {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) : TendstoUniformlyOn (fun (ε y : ℝ) => supOccupationResolvent θ q ε y) (supPotential θ q) (nhdsWithin 0 (Set.Ioi 0)) (Set.Ici 0)

Occupation potentials converge uniformly over all nonnegative starts.

theorem BGW.StableTrees.exists_forall_abs_supOccupationResolvent_sub_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {δ : ℝ} (hδ : 0 < δ) : ∃ (a : ℝ), 0 < a ∧ ∀ (ε η : ℝ), 0 < ε → ε < a → 0 < η → η < a → ∀ (y : ℝ), |supOccupationResolvent θ 1 ε y - supOccupationResolvent θ 1 η y| ≤ δ

Cauchy control at rate one is uniform over every real initial argument.