Uniform numerical occupation moment bounds

The rate-two occupation bound and the generic signed resolvent moment inequality give the constants required for the occupation Cauchy construction.

Reference: A. E. Kyprianou, Fluctuations of Lévy Processes with Applications, 2nd ed., Springer, 2014, Chapter 8.

theorem BGW.StableTrees.integral_exp_neg_two_supOccKernel_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : NNReal) {ε : ℝ} (hε : 0 < ε) : ∫ (f : Skorokhod.DLoc), ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-2 * t) * |supOccKernel ε (supReflectedFrom x f t.toNNReal)| ∂↑(stableLocalLaw θ) ≤ 1

The absolute rate-two occupation has expectation at most one.

theorem BGW.StableTrees.integral_sq_discountedOccupation_supOccupation_sub_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : NNReal) {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) {D : ℝ} (hD : ∀ (y : ℝ), |supOccupationResolvent θ 1 ε y - supOccupationResolvent θ 1 η y| ≤ D) : ∫ (f : Skorokhod.DLoc), Probability.discountedOccupation (fun (t : NNReal) (f : Skorokhod.DLoc) => supReflectedFrom x f t) (fun (r : ℝ) => supOccKernel ε r - supOccKernel η r) f ^ 2 ∂↑(stableLocalLaw θ) ≤ 4 * D

The second moment of an occupation difference is bounded by four times its potential bound.

theorem BGW.StableTrees.integral_sq_discountedOccupation_supOccupation_le_two {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : NNReal) {ε : ℝ} (hε : 0 < ε) : ∫ (f : Skorokhod.DLoc), Probability.discountedOccupation (fun (t : NNReal) (f : Skorokhod.DLoc) => supReflectedFrom x f t) (supOccKernel ε) f ^ 2 ∂↑(stableLocalLaw θ) ≤ 2

The second moment of a single positive occupation cutoff is at most two.