Small-jump moments of stable Lévy measures

On a neighbourhood of zero, the absolute qth jump moment of a non-Gaussian stable Lévy measure is finite exactly when α < q. Its value is independent of skewness and is a constant times r ^ (q - α). In particular, the small-jump second moment tends to zero, whereas the first absolute moment is finite exactly below shape one.

These estimates supply variance control for centered small-jump sums and first-moment control for identifying the support endpoints of one-sided stable laws. The proofs reuse the existing stable Lévy half-line decomposition and radial-power integrability, with Mathlib's sharp interval-power criterion and power integral.

References

• J. P. Nolan, Univariate Stable Distributions: Models for Heavy Tailed Data, Springer, 2020, chapter 1.

theorem TauCeti.Probability.integrableOn_abs_rpow_stableLevyMeasure {α β q : ℝ} (hα : α ∈ Set.Ioo 0 2) (hβ : |β| ≤ 1) (hq : α < q) (r : ℝ) : MeasureTheory.IntegrableOn (fun (x : ℝ) => |x| ^ q) (Metric.ball 0 r) (stableLevyMeasure α β)

Absolute jump powers above the stable shape are integrable on every bounded ball about zero. This is local integrability of the Lévy measure, rather than a stable-law moment.

theorem TauCeti.Probability.integrableOn_abs_rpow_stableLevyMeasure_iff {α β q r : ℝ} (hα : α ∈ Set.Ioo 0 2) (hβ : |β| ≤ 1) (hr : 0 < r) : MeasureTheory.IntegrableOn (fun (x : ℝ) => |x| ^ q) (Metric.ball 0 r) (stableLevyMeasure α β) ↔ α < q

The exact small-jump absolute-moment threshold. At the critical exponent the moment diverges, including for either fully skewed Lévy measure.

theorem TauCeti.Probability.integral_abs_rpow_stableLevyMeasure_ball {α β q r : ℝ} (hα : α ∈ Set.Ioo 0 2) (hβ : |β| ≤ 1) (hq : α < q) (hr : 0 ≤ r) : ∫ (x : ℝ) in Metric.ball 0 r, |x| ^ q ∂stableLevyMeasure α β = 2 * (Real.Gamma (1 + α) * Real.sin (Real.pi * α / 2) / Real.pi) * r ^ (q - α) / (q - α)

The small-jump absolute qth moment is independent of skewness. The strict exponent hypothesis ensures integrability, including at the singularity at zero.

theorem TauCeti.Probability.integrableOn_id_stableLevyMeasure_iff {α β r : ℝ} (hα : α ∈ Set.Ioo 0 2) (hβ : |β| ≤ 1) (hr : 0 < r) : MeasureTheory.IntegrableOn (fun (x : ℝ) => x) (Metric.ball 0 r) (stableLevyMeasure α β) ↔ α < 1

The identity is integrable against the stable Lévy measure on a positive-radius ball about zero exactly below shape one. Shape one belongs to the divergent side.

theorem TauCeti.Probability.integrableOn_sq_stableLevyMeasure (α β r : ℝ) : MeasureTheory.IntegrableOn (fun (x : ℝ) => x ^ 2) (Metric.ball 0 r) (stableLevyMeasure α β)

The small jumps of a stable Lévy measure have a finite second moment on every ball. The assertion includes the zero measures at invalid parameters.

theorem TauCeti.Probability.memLp_two_id_cond_stableLevyMeasure_smallJumpBand {α β ε r : ℝ} : MeasureTheory.MemLp id 2 (stableLevyMeasure α β)[|{x : ℝ | ε < |x| ∧ |x| ≤ r}]

The conditional law of jumps in any band has a finite second moment.

theorem TauCeti.Probability.integral_sq_stableLevyMeasure_ball {α β r : ℝ} (hα : α ∈ Set.Ioo 0 2) (hβ : |β| ≤ 1) (hr : 0 ≤ r) : ∫ (x : ℝ) in Metric.ball 0 r, x ^ 2 ∂stableLevyMeasure α β = 2 * (Real.Gamma (1 + α) * Real.sin (Real.pi * α / 2) / Real.pi) * r ^ (2 - α) / (2 - α)

The exact second moment of stable jumps smaller than r, the quantity controlling the variance of centered small-jump remainders.

theorem TauCeti.Probability.tendsto_integral_abs_rpow_stableLevyMeasure_ball_zero {α β q : ℝ} (hα : α ∈ Set.Ioo 0 2) (hβ : |β| ≤ 1) (hq : α < q) : Filter.Tendsto (fun (r : ℝ) => ∫ (x : ℝ) in Metric.ball 0 r, |x| ^ q ∂stableLevyMeasure α β) (nhdsWithin 0 (Set.Ici 0)) (nhds 0)

Every finite absolute small-jump moment vanishes as its cutoff shrinks to zero.

theorem TauCeti.Probability.tendsto_integral_sq_stableLevyMeasure_ball_zero {α β : ℝ} (hα : α ∈ Set.Ioo 0 2) (hβ : |β| ≤ 1) : Filter.Tendsto (fun (r : ℝ) => ∫ (x : ℝ) in Metric.ball 0 r, x ^ 2 ∂stableLevyMeasure α β) (nhdsWithin 0 (Set.Ici 0)) (nhds 0)

The variance contribution of jumps below a shrinking cutoff tends to zero.