Bounded stopping epochs and square integrability of the error

References

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

theorem BGW.StableTrees.errStopTime_le (n : ℕ) (σ : Skorokhod.DLoc → ENNReal) (t : NNReal) (f : Skorokhod.DLoc) : errStopTime n σ t f ≤ t

The bounded stopping epoch never exceeds its deterministic horizon.

theorem BGW.StableTrees.errStopTime_le_cutoff (n : ℕ) (σ : Skorokhod.DLoc → ENNReal) (t : NNReal) (f : Skorokhod.DLoc) : ↑(errStopTime n σ t f) ≤ errCutoff n f

The bounded stopping epoch never exceeds the localizing cutoff.

theorem BGW.StableTrees.errStopTime_eval_eq_stoppedProcess (F : NNReal → Skorokhod.DLoc → ℝ) (n : ℕ) (σ : Skorokhod.DLoc → ENNReal) (t : NNReal) (f : Skorokhod.DLoc) : F (errStopTime n σ t f) f = MeasureTheory.stoppedProcess F (fun (f : Skorokhod.DLoc) => min (σ f) (errCutoff n f)) t f

Evaluation at the finite epoch agrees with Mathlib's stopped-process representative.

theorem BGW.StableTrees.stronglyMeasurable_errStopTime_eval {F : NNReal → Skorokhod.DLoc → ℝ} (hF : MeasureTheory.IsStronglyProgressive Skorokhod.DLoc.filtration F) (n : ℕ) {σ : Skorokhod.DLoc → ENNReal} (hσ : MeasureTheory.IsStoppingTime Skorokhod.DLoc.filtration σ) (t : NNReal) : MeasureTheory.StronglyMeasurable fun (f : Skorokhod.DLoc) => F (errStopTime n σ t f) f

Progressive processes evaluated at the bounded epoch are measurable at that horizon.

theorem BGW.StableTrees.integrable_sq_errorMartingale_stopped {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ε : ℝ} (hε : 0 < ε) (n : ℕ) {σ : Skorokhod.DLoc → ENNReal} (hσ : MeasureTheory.IsStoppingTime Skorokhod.DLoc.filtration σ) (t : NNReal) : MeasureTheory.Integrable (fun (f : Skorokhod.DLoc) => errorMartingale θ ε (errStopTime n σ t f) f ^ 2) ↑(stableLocalLaw θ)

The stopped error has an integrable square at each bounded horizon.