Deterministic bounds for compact occupation errors

The same zero-start event gives the discount-removal bound at every horizon.

References

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

theorem BGW.StableTrees.compactError_nonneg {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) (T : NNReal) (f : Skorokhod.DLoc) : 0 ≤ compactError ε η T f

The compact error is nonnegative on every path.

theorem BGW.StableTrees.compactError_le {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) (T : NNReal) (f : Skorokhod.DLoc) : compactError ε η T f ≤ (ε⁻¹ + η⁻¹) * ↑T

A deterministic bound for the compact occupation error.

theorem BGW.StableTrees.integrable_sq_compactError (θ : ℝ) {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) (T : NNReal) : MeasureTheory.Integrable (fun (f : Skorokhod.DLoc) => compactError ε η T f ^ 2) ↑(stableLocalLaw θ)

Compact occupation errors have integrable squares at every pair of positive cutoffs.

theorem BGW.StableTrees.abs_occupationDiffMartingale_le {θ ε η D : ℝ} (hε : 0 < ε) (hη : 0 < η) (hD : ∀ (y : ℝ), |supOccupationResolvent θ 1 ε y - supOccupationResolvent θ 1 η y| ≤ D) {s T : NNReal} (hs : s ≤ T) (f : Skorokhod.DLoc) : |occupationDiffMartingale θ ε η s f| ≤ (ε⁻¹ + η⁻¹) * ↑T + D

An all-path compact bound for the explicit martingale.

theorem BGW.StableTrees.compactError_le_of_zero_start {θ ε η D : ℝ} (hε : 0 < ε) (hη : 0 < η) (hD : ∀ (y : ℝ), |supOccupationResolvent θ 1 ε y - supOccupationResolvent θ 1 η y| ≤ D) (f : Skorokhod.DLoc) (h0 : ↑f 0 = 0) (T : NNReal) : compactError ε η T f ≤ 2 * Real.exp ↑T * ((⨆ (t : ↑(Set.Iic T)), |occupationDiffMartingale θ ε η (↑t) f|) + D)

Discount removal on each zero-start path, simultaneously in the horizon.

theorem BGW.StableTrees.ae_compactError_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) {D : ℝ} (hD : ∀ (y : ℝ), |supOccupationResolvent θ 1 ε y - supOccupationResolvent θ 1 η y| ≤ D) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (T : NNReal), compactError ε η T f ≤ 2 * Real.exp ↑T * ((⨆ (t : ↑(Set.Iic T)), |occupationDiffMartingale θ ε η (↑t) f|) + D)

Deterministic integration by parts removes the discount on one common event.