Compact occupation errors and their resolvent martingale

The occupation Cauchy construction uses the reflected resolvent at rate one. It builds on BGW.StableTrees.SupremumPotential, BGW.StableTrees.SupremumReflectedFamily and the Doob estimates of BGW.Probability.DoobL2Resolvent.

References

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

noncomputable def BGW.StableTrees.compactError (ε η : ℝ) (T : NNReal) (f : Skorokhod.DLoc) : ℝ

sup_{t ≤ T} |O_ε(t) - O_η(t)|.

Equations

• BGW.StableTrees.compactError ε η T f = ⨆ (t : ↑(Set.Iic T)), |BGW.StableTrees.supOccupation ε f ↑t - BGW.StableTrees.supOccupation η f ↑t|

noncomputable def BGW.StableTrees.occupationDiffMartingale (θ ε η : ℝ) (t : NNReal) (f : Skorokhod.DLoc) : ℝ

The martingale J_t = ∫_0^t e^{-s}(g_ε-g_η)(R^0_s)ds + e^{-t}(u¹_ε-u¹_η)(R^0_t) (= E[B_ε - B_η | F_t]; the explicit version of martingale_discounted_resolvent).

Equations

• One or more equations did not get rendered due to their size.

def BGW.StableTrees.IsSupAuxEpsSeq (θ : ℝ) (ε : ℕ → ℝ) : Prop

A fast sequence: positive, strictly decreasing to 0, and for every k and every η ∈ (0, ε_k] the squared compact error on [0,k] is integrable with mean ≤ 16⁻ᵏ (summable errors on integer horizons; Borel–Cantelli with thresholds 2⁻ᵏ).

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.StableTrees.measurable_compactError {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) (T : NNReal) : Measurable (compactError ε η T)

The compact occupation error is Borel measurable.

theorem BGW.StableTrees.supOccupation_eq_integral_supOccKernel {ε : ℝ} (f : Skorokhod.DLoc) (h0 : ↑f 0 = 0) (t : NNReal) : supOccupation ε f t = ∫ (s : ℝ) in Set.Ioc 0 ↑t, supOccKernel ε (supReflectedFrom 0 f s.toNNReal)

Occupation is the time integral of its reflected kernel on zero-start paths.

theorem BGW.StableTrees.ae_supOccupation_eq_integral_supOccKernel {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ε : ℝ} (hε : 0 < ε) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (t : NNReal), supOccupation ε f t = ∫ (s : ℝ) in Set.Ioc 0 ↑t, supOccKernel ε (supReflectedFrom 0 f s.toNNReal)

O_ε(t) = ∫_0^t g_ε(R^0_s) ds for all t simultaneously, almost surely.

theorem BGW.StableTrees.martingale_occupationDiffMartingale {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) : MeasureTheory.Martingale (fun (t : NNReal) (f : Skorokhod.DLoc) => occupationDiffMartingale θ ε η t f) Skorokhod.DLoc.filtration ↑(stableLocalLaw θ)

The explicit occupation resolvent process is a martingale.

theorem BGW.StableTrees.rightContinuous_occupationDiffMartingale {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) (f : Skorokhod.DLoc) (t : NNReal) : ContinuousWithinAt (fun (s : NNReal) => occupationDiffMartingale θ ε η s f) (Set.Ici t) t

Every path of the occupation resolvent martingale is right continuous.