Compact and tail bounds for weighted occupation error

The estimate uses compact square error and the half-rate occupation and clock means. No expectation is interchanged with a path-dependent weight measure.

theorem BGW.StableTrees.ae_abs_supWeightedOccupation_sub_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam ε δ : ℝ} (hq : 0 < q) (hlam : 0 ≤ lam) (hε : 0 < ε) (hδ : 0 < δ) (T : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), |supWeightedOccupation q lam ε f - (supBoundaryPotential θ q lam f).toReal| ≤ δ + supAuxApproxError θ ε T f ^ 2 / δ + Real.exp (-(q / 2) * ↑T) * (supAuxOccupationTail (q / 2) ε 0 f + supAuxDiscountedTail θ (q / 2) 0 f)

A pathwise compact-error and half-rate-tail estimate for weighted occupations.

Reference: Bertoin, Lévy Processes, Chapter VI.

theorem BGW.StableTrees.integral_abs_supWeightedOccupation_sub_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam ε δ : ℝ} (hq : 0 < q) (hlam : 0 ≤ lam) (hε : 0 < ε) (hδ : 0 < δ) (T : NNReal) : ∫ (f : Skorokhod.DLoc), |supWeightedOccupation q lam ε f - (supBoundaryPotential θ q lam f).toReal| ∂↑(stableLocalLaw θ) ≤ δ + (∫ (f : Skorokhod.DLoc), supAuxApproxError θ ε T f ^ 2 ∂↑(stableLocalLaw θ)) / δ + Real.exp (-(q / 2) * ↑T) * (2 * ((q / 2) ^ (1 / θ) / (q / 2)))

The weighted approximation error has a mean bound with a vanishing compact term and an exponentially small tail, uniform in the occupation cutoff.

Reference: Bertoin, Lévy Processes, Chapter VI.