Measurability and Tonelli for ladder potentials

Inverse substitution gives measurability of the pathwise boundary integral, without a measurability assertion about the totalized random Stieltjes measure.

theorem BGW.StableTrees.aemeasurable_supBoundaryPotential {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam : ℝ} (hq : 0 ≤ q) (hlam : 0 ≤ lam) : AEMeasurable (supBoundaryPotential θ q lam) ↑(stableLocalLaw θ)

The extended boundary potential is almost everywhere measurable at nonnegative rates.

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

theorem BGW.StableTrees.integrable_exp_neg_supLadder {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam : ℝ} (hq : 0 ≤ q) (hlam : 0 ≤ lam) (z : NNReal) : MeasureTheory.Integrable (fun (f : Skorokhod.DLoc) => Real.exp (-q * ↑(supLadderTime θ z f) - lam * supLadderHeight θ z f)) ↑(stableLocalLaw θ)

The ladder exponential is integrable at nonnegative rates.

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

theorem BGW.StableTrees.lintegral_supLadderLaplace_eq {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam : ℝ} (hq : 0 ≤ q) (hlam : 0 ≤ lam) : ∫⁻ (z : ℝ) in Set.Ioi 0, ENNReal.ofReal (supLadderLaplace θ q lam z.toNNReal) = ∫⁻ (f : Skorokhod.DLoc), supBoundaryPotential θ q lam f ∂↑(stableLocalLaw θ)

Tonelli: ∫_0^∞ φ(z) dz = E ∫_0^∞ e^{-qA_z - λB_z} dz = E ∫ e^{-qt-λS_t} dM_t.