The normalized boundary potential

The compact error tends to zero first, and the half-rate bound then removes the tail. Exponential-clock independence identifies the resulting finite mean.

theorem BGW.StableTrees.tendsto_integral_abs_supWeightedOccupation_sub {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam : ℝ} (hq : 0 < q) (hlam : 0 ≤ lam) : Filter.Tendsto (fun (ε : ℝ) => ∫ (f : Skorokhod.DLoc), |supWeightedOccupation q lam ε f - (supBoundaryPotential θ q lam f).toReal| ∂↑(stableLocalLaw θ)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Weighted occupations converge in mean to the real boundary potential.

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

theorem BGW.StableTrees.lintegral_supBoundaryPotential_eq {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam : ℝ} (hq : 0 < q) (hlam : 0 ≤ lam) : ∫⁻ (f : Skorokhod.DLoc), supBoundaryPotential θ q lam f ∂↑(stableLocalLaw θ) = ENNReal.ofReal (q ^ (1 / θ) / q * ∫ (p : Skorokhod.DLoc × ℝ), Real.exp (-lam * supRunning p.1 p.2.toNNReal) ∂expClockLaw θ q)

Boundary potential, mean form. For q > 0, λ ≥ 0: E ∫_0^∞ e^{-qt-λS_t} dM_t = (Φ/q) E e^{-λ S_{e_q}} (cumulative Tonelli representation, compact square-mean occupation error, and half-rate control of the tail, along the full positive-cutoff filter).

theorem BGW.StableTrees.lintegral_supBoundaryPotential {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam : ℝ} (hq : 0 < q) (hlam : 0 ≤ lam) : ∫⁻ (f : Skorokhod.DLoc), supBoundaryPotential θ q lam f ∂↑(stableLocalLaw θ) = ENNReal.ofReal (supLadderExponent θ q lam)⁻¹

Boundary potential, exact form: E ∫_0^∞ e^{-qt-λS_t} dM_t = 1/κ(q,λ).