Exact ascending ladder transform

The finite positive boundary potential identifies the semigroup rate, fixing the normalization without an adjustable multiplicative constant.

theorem BGW.StableTrees.supLadderLaplace_eq_of_pos {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam : ℝ} (hq : 0 < q) (hlam : 0 ≤ lam) (z : NNReal) : supLadderLaplace θ q lam z = Real.exp (-↑z * supLadderExponent θ q lam)

Exact normalization for q > 0: φ(z) = exp(-z κ(q,λ)), c = 1.

theorem BGW.StableTrees.supLadderLaplace_eq {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam : ℝ} (hq : 0 ≤ q) (hlam : 0 ≤ lam) (z : NNReal) : supLadderLaplace θ q lam z = Real.exp (-↑z * supLadderExponent θ q lam)

Exact transform for all q, λ ≥ 0 (including q = 0 and (0,0)).

theorem BGW.StableTrees.supLadderLaplace_diagonal {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 ≤ q) (z : NNReal) : supLadderLaplace θ q (q ^ (1 / θ)) z = Real.exp (-↑z * (θ * q ^ (1 - 1 / θ)))

Diagonal value: E exp(-q A_z - q^{1/θ} B_z) = exp(-z θ q^{1-1/θ}) (from supLadderExponent_diagonal).

theorem BGW.StableTrees.integral_exp_neg_supLadder {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (z : NNReal) {q lam : ℝ} (hq : 0 ≤ q) (hlam : 0 ≤ lam) : ∫ (f : Skorokhod.DLoc), Real.exp (-q * ↑(supLadderTime θ z f) - lam * supLadderHeight θ z f) ∂↑(stableLocalLaw θ) = Real.exp (-↑z * supLadderExponent θ q lam) ∧ ∫ (f : Skorokhod.DLoc), Real.exp (-q * ↑(supLadderTime θ z f)) ∂↑(stableLocalLaw θ) = Real.exp (-↑z * q ^ (1 - 1 / θ)) ∧ ∫ (f : Skorokhod.DLoc), Real.exp (-lam * supLadderHeight θ z f) ∂↑(stableLocalLaw θ) = Real.exp (-↑z * lam ^ (θ - 1))

Joint ladder transform (normalization c = 1) at every deterministic level z ≥ 0, and its two marginals (κ(q,0) = q^{1-1/θ}, κ(0,λ) = λ^{θ-1}): E exp(-q A_z - λ B_z) = exp(-z κ(q, λ)) for q, λ ≥ 0.

References: Bertoin, Lévy Processes, Chapter VI; Kyprianou, Fluctuations of Lévy Processes with Applications, Chapter 6.