Maximal bounded stopped energy #
Doob's inequality is applied with the almost sure right-continuity event of the error.
References #
- J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.
theorem
BGW.StableTrees.integral_sq_sup_errorMartingale_stopped_le
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
{ε : ℝ}
(hε : 0 < ε)
(z : NNReal)
(n : ℕ)
(t : NNReal)
:
MeasureTheory.Integrable
(fun (f : Skorokhod.DLoc) =>
(⨆ (s : ↑(Set.Iic t)), |errorMartingale θ ε (errStopTime n (supHitting θ z) (↑s) f) f|) ^ 2)
↑(stableLocalLaw θ) ∧ ∫ (f : Skorokhod.DLoc), (⨆ (s : ↑(Set.Iic t)), |errorMartingale θ ε (errStopTime n (supHitting θ z) (↑s) f) f|) ^ 2 ∂↑(stableLocalLaw θ) ≤ 4 * (4 * ↑z * supCorrectionBound θ ε + 12 * supCorrectionBound θ ε ^ 2)
Doob L² maximal inequality for the stopped D:
E sup_{s ≤ t}|D_{s∧τ_n}|² ≤ 4 E D_{t∧τ_n}² ≤ 4 (4 z V + 12 V²).