Compact square-mean Cauchy estimates

The explicit constant combines the compact Doob inequality with discount removal.

References

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

theorem BGW.StableTrees.integral_sq_compactError_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) => compactError ε η T f ^ 2) ↑(stableLocalLaw θ) ∧ ∫ (f : Skorokhod.DLoc), compactError ε η T f ^ 2 ∂↑(stableLocalLaw θ) ≤ 128 * Real.exp (2 * ↑T) * (D + D ^ 2)

Explicit compact L² estimate: E sup_{t≤T}|O_ε-O_η|² ≤ 128 e^{2T}(D + D²) whenever ‖u¹_ε-u¹_η‖_∞ ≤ D, uniformly in the initial state 0, with integrability.

theorem BGW.StableTrees.supOccupation_compact_L2_cauchy {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (T : NNReal) (δ : ℝ) : 0 < δ → ∃ (a : ℝ), 0 < a ∧ ∀ (ε η : ℝ), 0 < ε → ε < a → 0 < η → η < a → MeasureTheory.Integrable (fun (f : Skorokhod.DLoc) => compactError ε η T f ^ 2) ↑(stableLocalLaw θ) ∧ ∫ (f : Skorokhod.DLoc), compactError ε η T f ^ 2 ∂↑(stableLocalLaw θ) ≤ δ

Compact-time Cauchy estimate.