The ladder Laplace semigroup

Stationary independent increments give multiplicativity of the ladder Laplace functional.

theorem BGW.StableTrees.supLadderLaplace_add {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam : ℝ} (hq : 0 ≤ q) (hlam : 0 ≤ lam) (y z : NNReal) : supLadderLaplace θ q lam (y + z) = supLadderLaplace θ q lam y * supLadderLaplace θ q lam z

Multiplicativity: φ(y + z) = φ(y) φ(z) (restart at A_y, independent stationary increments, BGW.StableTrees.SupremumLadderRestart).

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

theorem BGW.StableTrees.tendsto_supLadderLaplace_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam : ℝ} (hq : 0 ≤ q) (hlam : 0 ≤ lam) : Filter.Tendsto (supLadderLaplace θ q lam) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)

Right continuity at 0 (right continuity of (A,B) and bounded convergence).