Real compact Doob estimates for occupation differences #
The extended compact maximal inequality is converted to an integrable real supremum.
References #
- [J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV]
theorem
BGW.StableTrees.integral_sq_sup_Iic_le_four_mul
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{ℱ : MeasureTheory.Filtration NNReal inst✝}
{M : NNReal → Ω → ℝ}
(hM : MeasureTheory.Martingale M ℱ μ)
(hrc : ∀ (ω : Ω) (t : NNReal), ContinuousWithinAt (fun (s : NNReal) => M s ω) (Set.Ici t) t)
(T : NNReal)
(h2 : MeasureTheory.Integrable (fun (ω : Ω) => M T ω ^ 2) μ)
:
Real compact Doob inequality, with square integrability of the supremum.
theorem
BGW.StableTrees.integral_sq_sup_occupationDiffMartingale_le
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
{ε η : ℝ}
(hε : 0 < ε)
(hη : 0 < η)
{D : ℝ}
(hD : ∀ (y : ℝ), |supOccupationResolvent θ 1 ε y - supOccupationResolvent θ 1 η y| ≤ D)
(T : NNReal)
:
MeasureTheory.Integrable
(fun (f : Skorokhod.DLoc) => (⨆ (t : ↑(Set.Iic T)), |occupationDiffMartingale θ ε η (↑t) f|) ^ 2)
↑(stableLocalLaw θ) ∧ ∫ (f : Skorokhod.DLoc), (⨆ (t : ↑(Set.Iic T)), |occupationDiffMartingale θ ε η (↑t) f|) ^ 2 ∂↑(stableLocalLaw θ) ≤ 16 * D
Doob L² on compacts: a uniform resolvent difference bound controls the maximum.