Continuity and the Brownian case of the supremum correction

The positive-part power representation makes the zero-rate scale continuous.

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

theorem BGW.StableTrees.continuous_stableScale {θ : ℝ} (hθ : 1 < θ) : Continuous (stableScale θ)

The zero-rate scale is continuous through its zero extension.

theorem BGW.StableTrees.continuousOn_supCorrection {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ε : ℝ} (hε : 0 < ε) : ContinuousOn (supCorrection θ ε) (Set.Ici 0)

Continuity of the correction on nonnegative starting states.

theorem BGW.StableTrees.supCorrection_two {ε : ℝ} (hε : 0 < ε) {y : ℝ} (hy : 0 ≤ y) : supCorrection 2 ε y = -(max (ε - y) 0 ^ 2 / (2 * ε))

Brownian case: v_ε(y) = -(ε-y)_+² / (2ε).

theorem BGW.StableTrees.abs_supCorrection_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ε : ℝ} (hε : 0 < ε) {y : ℝ} (hy : 0 ≤ y) : |supCorrection θ ε y| ≤ (1 / Real.Gamma θ + 1 / 2) * ε ^ (θ - 1)

|v_ε| ≤ (1/Γ(θ) + 1/2) ε^{θ-1} for every ε > 0, y ≥ 0.