Centered zero-rate limit of the error process

References

• J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.

theorem BGW.StableTrees.ae_tendsto_discountedErrorMartingale {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ε : ℝ} (hε : 0 < ε) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (t : NNReal), Filter.Tendsto (fun (q : ℝ) => discountedErrorMartingale θ q ε t f - (supOccupationResolvent θ q ε 0 - supPotential θ q 0)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (errorMartingale θ ε t f))

The centered positive-rate errors converge at all times on a single full-measure event.