Height increment moments

Normalize increments by their stable height scale and integrate the exponential tail. Integrability is established before using the Bochner integral.

theorem BGW.StableTrees.height_increment_moment_bound {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {p : ℝ} (hp : 1 ≤ p) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (t s : NNReal), 0 < s → MeasureTheory.Integrable (fun (f : Skorokhod.DLoc) => |height θ f (t + s) - height θ f t| ^ p) ↑(stableLocalLaw θ) ∧ ∫ (f : Skorokhod.DLoc), |height θ f (t + s) - height θ f t| ^ p ∂↑(stableLocalLaw θ) ≤ C * ↑s ^ (p * (1 - 1 / θ))

Increment moments with one constant for all t and s: E|H_{t+s} - H_t|^p ≤ C s^(p (1 - 1/θ)), the integrand being integrable.