Zero-resolvent correction and discounted error processes

Definitions of the centered error and its positive-rate approximants, and elementary bounds for the correction. The auxiliary clock retains its raw adapted representative.

References

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

noncomputable def BGW.StableTrees.supCorrectionBound (θ ε : ℝ) : ℝ

V_ε = (1/Γ(θ) + 1/2) ε^{θ-1}: explicit bound for sup_{y ≥ 0} |v_ε(y)|.

Equations

• BGW.StableTrees.supCorrectionBound θ ε = (1 / Real.Gamma θ + 1 / 2) * ε ^ (θ - 1)

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

The correction increment w_t = v_ε(R_t) - v_ε(0), R_t = R^0_t.

Equations

• BGW.StableTrees.occupationCorrection θ ε t f = BGW.StableTrees.supCorrection θ ε (BGW.StableTrees.supReflectedFrom 0 f t) - BGW.StableTrees.supCorrection θ ε 0

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

The error process D_t = O_ε(t) - M^*_t + v_ε(R_t) - v_ε(0), with M^* = supAuxLocalTime.

Equations

• BGW.StableTrees.errorMartingale θ ε t f = BGW.StableTrees.supOccupation ε f t - BGW.StableTrees.supAuxLocalTime θ f t + BGW.StableTrees.occupationCorrection θ ε t f

noncomputable def BGW.StableTrees.supAuxDiscountedHead (θ q : ℝ) (t : NNReal) (f : Skorokhod.DLoc) : ℝ

Discounted head of the clock, ∫_{(0,t]} e^{-qs} dM^*_s, by integration by parts (M^*_0 = 0): e^{-qt} M^*_t + q ∫_0^t e^{-qs} M^*_s ds. Adapted for every path.

Equations

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

noncomputable def BGW.StableTrees.supOccupationDiscountedHead (q ε : ℝ) (t : NNReal) (f : Skorokhod.DLoc) : ℝ

Discounted head of the occupation, O^q_t = ∫_0^t e^{-qs} g_ε(R^0_s) ds.

Equations

• BGW.StableTrees.supOccupationDiscountedHead q ε t f = ∫ (s : ℝ) in Set.Ioc 0 ↑t, Real.exp (-q * s) * BGW.StableTrees.supOccKernel ε (BGW.StableTrees.supReflectedFrom 0 f s.toNNReal)

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

Positive-rate error martingale N^q_t = O^q_t - M^q_t + e^{-qt} (u^q_ε - h_q)(R_t).

Equations

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

noncomputable def BGW.StableTrees.supReflectedExit (K : ℝ) (f : Skorokhod.DLoc) : ENNReal

Strict exit time τ_K = inf{t | R^0_t > K} (⊤ if never).

Equations

• BGW.StableTrees.supReflectedExit K f = ⨅ (t : NNReal), if K < BGW.StableTrees.supReflectedFrom 0 f t then ↑t else ⊤

noncomputable def BGW.StableTrees.errCutoff (n : ℕ) (f : Skorokhod.DLoc) : ENNReal

The localizing cutoff min (τ_n) n (independent of the inverse clock).

Equations

• BGW.StableTrees.errCutoff n f = min (BGW.StableTrees.supReflectedExit (↑n) f) ↑n

noncomputable def BGW.StableTrees.errStopTime (n : ℕ) (σ : Skorokhod.DLoc → ENNReal) (t : NNReal) (f : Skorokhod.DLoc) : NNReal

The stopping epoch min (min t σ) (cutoff n) as a finite time.

Equations

• BGW.StableTrees.errStopTime n σ t f = (min (min (↑t) (σ f)) (BGW.StableTrees.errCutoff n f)).toNNReal

theorem BGW.StableTrees.measurable_supCorrection (θ ε : ℝ) : Measurable (supCorrection θ ε)

The correction is Borel measurable, including outside the stable parameter range.

theorem BGW.StableTrees.abs_occupationCorrection_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ε : ℝ} (hε : 0 < ε) (t : NNReal) (f : Skorokhod.DLoc) : |occupationCorrection θ ε t f| ≤ 2 * supCorrectionBound θ ε

The correction increment is bounded uniformly in the path and time.

theorem BGW.StableTrees.occupationCorrection_eq_zero {θ ε : ℝ} {t : NNReal} {f : Skorokhod.DLoc} (h : supReflectedFrom 0 f t = 0) : occupationCorrection θ ε t f = 0

The correction increment vanishes on the contact set.

theorem BGW.StableTrees.tendsto_supCorrectionBound {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : Filter.Tendsto (supCorrectionBound θ) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

The uniform correction bound vanishes as the occupation width tends to zero.

theorem BGW.StableTrees.errCutoff_le (n : ℕ) (f : Skorokhod.DLoc) : errCutoff n f ≤ ↑n

The cutoff is bounded by its deterministic integer horizon.

theorem BGW.StableTrees.monotone_errCutoff (f : Skorokhod.DLoc) : Monotone fun (n : ℕ) => errCutoff n f

The cutoffs increase with their integer level.