The zero-rate limit of the occupation correction

The scalar boundary term is a derivative of an averaged exponential at zero.

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

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

The zero-rate occupation correction converges locally uniformly in the nonnegative start.