Elementary properties of the ladder Laplace functional

Measurability, bounds and bounded convergence for the ascending ladder pair.

theorem BGW.StableTrees.supLadderLaplace_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (q lam : ℝ) : supLadderLaplace θ q lam 0 = 1

The ladder Laplace functional equals one at level zero.

theorem BGW.StableTrees.supLadderLaplace_mem_Icc {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam : ℝ} (hq : 0 ≤ q) (hlam : 0 ≤ lam) (z : NNReal) : supLadderLaplace θ q lam z ∈ Set.Icc 0 1

The nonnegative-rate ladder Laplace functional lies between zero and one.

theorem BGW.StableTrees.measurable_supLadderLaplace {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (q lam : ℝ) : Measurable (supLadderLaplace θ q lam)

The ladder Laplace functional is measurable in the level.

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

theorem BGW.StableTrees.tendsto_supLadderLaplace_zero_rate {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {lam : ℝ} (hlam : 0 ≤ lam) (z : NNReal) : Filter.Tendsto (fun (q : ℝ) => supLadderLaplace θ q lam z) (nhdsWithin 0 (Set.Ioi 0)) (nhds (supLadderLaplace θ 0 lam z))

Bounded convergence in q ↓ 0 at fixed level (A_z < ∞ a.s.).

theorem BGW.StableTrees.ae_supLadder_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), supLadderTime θ 0 f = 0 ∧ supLadderHeight θ 0 f = 0

Start at the origin: A_0 = 0 = B_0 almost surely.