Positive jumps of the stable process: Laplace and tail estimates

This module computes the second difference of the stable Laplace transform and derives the frequent polynomial lower bound for the positive tail needed to detect jumps of the host process.

theorem BGW.StableTrees.integrable_exp_neg_mul_stableLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {lam : ℝ} (hlam : 0 ≤ lam) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (-lam * x)) ↑(stableLaw θ)

x ↦ e^{-λx} is integrable under the stable law for λ ≥ 0 (its integral e^{λ^θ} is nonzero).

theorem BGW.StableTrees.integral_one_sub_exp_sq_stableLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {lam : ℝ} (hlam : 0 ≤ lam) : ∫ (x : ℝ), (1 - Real.exp (-lam * x)) ^ 2 ∂↑(stableLaw θ) = Real.exp ((2 * lam) ^ θ) - 2 * Real.exp (lam ^ θ) + 1

Second difference of the Laplace transform: E(1 - e^{-λX})^2 = e^{(2λ)^θ} - 2e^{λ^θ} + 1.

theorem BGW.StableTrees.frequently_le_rpow_mul_stableLaw_Ioi {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hθ2 : θ < 2) : ∃ (c : ℝ), 0 < c ∧ ∃ᶠ (x : ℝ) in Filter.atTop, c ≤ x ^ θ * (↑(stableLaw θ)).real (Set.Ioi x)

Tail lower bound for 1 < θ < 2: limsup_{x→∞} x^θ P(X_1 > x) > 0.