Mean convergence of weighted boundary potentials

Compact square-mean occupation errors and the half-rate potential bound control the weighted cumulative error before identifying the exact mean potential.

theorem BGW.StableTrees.ae_supBoundaryPotential_cumulative {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam : ℝ} (hq : 0 < q) (hlam : 0 ≤ lam) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), have J := ∫ (s : ℝ) in Set.Ioi 0, supAuxLocalTime θ f s.toNNReal ∂(supWeightStieltjes q lam ⋯ hlam f).measure; supBoundaryPotential θ q lam f = ENNReal.ofReal J ∧ (supBoundaryPotential θ q lam f).toReal = J ∧ J ≤ supAuxDiscountedTail θ (q / 2) 0 f

The boundary potential has a finite cumulative representative bounded by the half-rate auxiliary potential.

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

theorem BGW.StableTrees.integrable_supBoundaryPotential_toReal {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam : ℝ} (hq : 0 < q) (hlam : 0 ≤ lam) : MeasureTheory.Integrable (fun (f : Skorokhod.DLoc) => (supBoundaryPotential θ q lam f).toReal) ↑(stableLocalLaw θ)

The real boundary potential is integrable at positive time rate.

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