Stopped maximal occupation error

The centered correction transfers Doob's estimate from the martingale to the occupation error. Eventual equality of the stopped suprema removes localization by Fatou.

References

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

theorem BGW.StableTrees.aestronglyMeasurable_sup_Iic_abs_of_ae_rightContinuous {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : NNReal → Ω → ℝ} (hX : ∀ (s : NNReal), Measurable (X s)) (hr : ∀ᵐ (ω : Ω) ∂μ, ∀ (s : NNReal), ContinuousWithinAt (fun (u : NNReal) => X u ω) (Set.Ici s) s) (T : NNReal) : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => ⨆ (s : ↑(Set.Iic T)), |X (↑s) ω|) μ

Almost sure right continuity makes the real compact absolute supremum measurable up to a null set, even for representatives with exceptional paths.

theorem BGW.StableTrees.integral_sq_sup_supOccupation_sub_supAuxLocalTime_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ε : ℝ} (hε : 0 < ε) (z : NNReal) : MeasureTheory.Integrable (fun (f : Skorokhod.DLoc) => (⨆ (t : ↑(Set.Iic (supAuxLadderTime θ z f))), |supOccupation ε f ↑t - supAuxLocalTime θ f ↑t|) ^ 2) ↑(stableLocalLaw θ) ∧ ∫ (f : Skorokhod.DLoc), (⨆ (t : ↑(Set.Iic (supAuxLadderTime θ z f))), |supOccupation ε f ↑t - supAuxLocalTime θ f ↑t|) ^ 2 ∂↑(stableLocalLaw θ) ≤ 104 * (↑z * supCorrectionBound θ ε + supCorrectionBound θ ε ^ 2)

Stopped maximal estimate: E sup_{t ≤ A^*_z}|O_ε(t) - M^*_t|² ≤ 104 (z V_ε + V_ε²) (O - M^* = D - w, |w| ≤ 2V).