State and time localization of the error process

References

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

theorem BGW.StableTrees.isStoppingTime_supReflectedExit (K : ℝ) : MeasureTheory.IsStoppingTime Skorokhod.DLoc.filtration (supReflectedExit K)

Strict reflected exits are stopping times of the right continuous filtration.

theorem BGW.StableTrees.isStoppingTime_errCutoff (n : ℕ) : MeasureTheory.IsStoppingTime Skorokhod.DLoc.filtration (errCutoff n)

The cutoff combines a state exit and a deterministic stopping horizon.

theorem BGW.StableTrees.ae_supReflectedFrom_le_of_le_errCutoff {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (n : ℕ) (t : NNReal), ↑t ≤ errCutoff n f → supReflectedFrom 0 f t ≤ ↑n

No-positive-jump reflection stays below the cutoff even at its exit epoch.