Right continuity of the positive-rate errors

References

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

theorem BGW.StableTrees.ae_rightContinuous_discountedErrorMartingale {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q ε : ℝ} (hq : 0 < q) (hε : 0 < ε) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (t : NNReal), ContinuousWithinAt (fun (s : NNReal) => discountedErrorMartingale θ q ε s f) (Set.Ici t) t

Almost surely the positive-rate process is right continuous at all times.