The Lévy measure of a scalar stable law

For 0 < α < 2 and |β| ≤ 1, the stable Lévy measure has density proportional to |x| ^ (-1 - α), with respective weights 1 + β and 1 - β on the positive and negative half-lines. It has no atom at zero. Parameters outside this non-Gaussian range give the zero measure.

Restricting to either tail gives a multiple of a Pareto law or its reflection, and at full skewness |β| = 1 the measure lives on a single half-line. In particular, removing a positive neighbourhood of zero leaves positive finite mass, and conditioning on that set gives a probability jump law for compound Poisson approximations. The absolute jump size under this conditioned law is Pareto, independently of skewness.

Integrability against the Lévy measure is Lebesgue integrability after multiplying by the density, and integrals against it split into power-weighted integrals over the two half-lines.

References

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

The tail normalization reuses Mathlib's paretoMeasure and its probability theorem.

noncomputable def TauCeti.Probability.stableLevyDensity (α β x : ℝ) : ℝ

The real density of the stable Lévy measure, with value zero at zero and outside 0 < α < 2, |β| ≤ 1. This is a Lévy density, rather than a probability density.

noncomputable def TauCeti.Probability.stableLevyMeasure (α β : ℝ) : MeasureTheory.Measure ℝ

The stable Lévy measure. Its restrictions away from zero supply finite jump measures.

theorem TauCeti.Probability.stableLevyMeasure_def (α β : ℝ) : stableLevyMeasure α β = MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (stableLevyDensity α β x)

The stable Lévy measure is Lebesgue measure weighted by its real density.

@[simp]

theorem TauCeti.Probability.stableLevyDensity_zero (α β : ℝ) : stableLevyDensity α β 0 = 0

theorem TauCeti.Probability.stableLevyDensity_of_ne_zero {α β : ℝ} (hα : α ∈ Set.Ioo 0 2) (hβ : |β| ≤ 1) {x : ℝ} (hx : x ≠ 0) : stableLevyDensity α β x = (Real.Gamma (1 + α) * Real.sin (Real.pi * α / 2) / Real.pi * if 0 < x then 1 + β else 1 - β) * |x| ^ (-(α + 1))

In the non-Gaussian range, the Lévy density has the prescribed power-law expression off zero.

@[simp]

theorem TauCeti.Probability.stableLevyDensity_eq_zero_of_not {α β : ℝ} (h : ¬(0 < α ∧ α < 2 ∧ |β| ≤ 1)) (x : ℝ) : stableLevyDensity α β x = 0

Parameters outside the non-Gaussian range give the zero Lévy density.

@[simp]

theorem TauCeti.Probability.stableLevyMeasure_eq_zero_of_not {α β : ℝ} (h : ¬(0 < α ∧ α < 2 ∧ |β| ≤ 1)) : stableLevyMeasure α β = 0

Parameters outside the non-Gaussian range give the zero Lévy measure.

theorem TauCeti.Probability.stableLevyDensity_coefficient_pos {α : ℝ} (hα : α ∈ Set.Ioo 0 2) : 0 < Real.Gamma (1 + α) * Real.sin (Real.pi * α / 2) / Real.pi

The normalizing coefficient of a non-Gaussian stable Lévy density is positive.

theorem TauCeti.Probability.stableLevyDensity_nonneg (α β x : ℝ) : 0 ≤ stableLevyDensity α β x

The real Lévy density is nonnegative for all parameters.

theorem TauCeti.Probability.measurable_stableLevyDensity : Measurable fun (p : (ℝ × ℝ) × ℝ) => stableLevyDensity p.1.1 p.1.2 p.2

The Lévy density is jointly measurable in both shapes and the jump size.

theorem TauCeti.Probability.measurable_stableLevyDensity_apply (α β : ℝ) : Measurable (stableLevyDensity α β)

For fixed shapes, the Lévy density is measurable in the jump size.

theorem TauCeti.Probability.measurable_stableLevyMeasure : Measurable fun (p : ℝ × ℝ) => stableLevyMeasure p.1 p.2

The full totalized Lévy measure family is Giry measurable.

instance TauCeti.Probability.instNullSingletonClassRealStableLevyMeasure (α β : ℝ) : MeasureTheory.NullSingletonClass (stableLevyMeasure α β)

The stable Lévy measure has no atoms.

instance TauCeti.Probability.instSigmaFiniteRealStableLevyMeasure (α β : ℝ) : MeasureTheory.SigmaFinite (stableLevyMeasure α β)

The stable Lévy measure is sigma-finite for all parameters.

@[simp]

theorem TauCeti.Probability.stableLevyDensity_neg (α β x : ℝ) : stableLevyDensity α β (-x) = stableLevyDensity α (-β) x

Reflection changes the sign of the skewness parameter in the Lévy density.

theorem TauCeti.Probability.map_neg_stableLevyMeasure (α β : ℝ) : MeasureTheory.Measure.map (fun (x : ℝ) => -x) (stableLevyMeasure α β) = stableLevyMeasure α (-β)

Reflecting the stable Lévy measure negates its skewness.

theorem TauCeti.Probability.stableLevyMeasure_restrict_Ioi {α β ε : ℝ} (hα : α ∈ Set.Ioo 0 2) (hβ : |β| ≤ 1) (hε : 0 < ε) : (stableLevyMeasure α β).restrict (Set.Ioi ε) = ENNReal.ofReal (Real.Gamma (1 + α) * Real.sin (Real.pi * α / 2) / Real.pi * (1 + β) / (α * ε ^ α)) • ProbabilityTheory.paretoMeasure ε α

Above a positive cutoff, the stable Lévy measure is a finite multiple of a Pareto law. This includes zero positive-tail mass at skewness -1.

theorem TauCeti.Probability.stableLevyMeasure_Ioi {α β ε : ℝ} (hα : α ∈ Set.Ioo 0 2) (hβ : |β| ≤ 1) (hε : 0 < ε) : (stableLevyMeasure α β) (Set.Ioi ε) = ENNReal.ofReal (Real.Gamma (1 + α) * Real.sin (Real.pi * α / 2) / Real.pi * (1 + β) / (α * ε ^ α))

The mass above a positive cutoff, including the vanishing tail at skewness -1.

theorem TauCeti.Probability.stableLevyMeasure_restrict_Iio {α β ε : ℝ} (hα : α ∈ Set.Ioo 0 2) (hβ : |β| ≤ 1) (hε : 0 < ε) : (stableLevyMeasure α β).restrict (Set.Iio (-ε)) = ENNReal.ofReal (Real.Gamma (1 + α) * Real.sin (Real.pi * α / 2) / Real.pi * (1 - β) / (α * ε ^ α)) • MeasureTheory.Measure.map (fun (x : ℝ) => -x) (ProbabilityTheory.paretoMeasure ε α)

Below a negative cutoff, the stable Lévy measure is a finite multiple of a reflected Pareto law. This includes zero negative-tail mass at skewness 1.

theorem TauCeti.Probability.stableLevyMeasure_Iio {α β ε : ℝ} (hα : α ∈ Set.Ioo 0 2) (hβ : |β| ≤ 1) (hε : 0 < ε) : (stableLevyMeasure α β) (Set.Iio (-ε)) = ENNReal.ofReal (Real.Gamma (1 + α) * Real.sin (Real.pi * α / 2) / Real.pi * (1 - β) / (α * ε ^ α))

The mass below a negative cutoff, including the vanishing tail at skewness 1.

theorem TauCeti.Probability.ae_mul_nonpos_stableLevyMeasure {α β t : ℝ} (hβ : |β| = 1) (ht : β * t ≤ 0) : ∀ᵐ (x : ℝ) ∂stableLevyMeasure α β, t * x ≤ 0

At full skewness the stable Lévy measure lives on one half-line: if β * t ≤ 0, then t * x ≤ 0 for almost every jump x.

theorem TauCeti.Probability.stableLevyMeasure_abs_gt {α β ε : ℝ} (hα : α ∈ Set.Ioo 0 2) (hβ : |β| ≤ 1) (hε : 0 < ε) : (stableLevyMeasure α β) {x : ℝ | ε < |x|} = ENNReal.ofReal (2 * Real.Gamma (1 + α) * Real.sin (Real.pi * α / 2) / (Real.pi * α * ε ^ α))

Removing a positive neighbourhood of zero leaves finite mass independent of skewness.

theorem TauCeti.Probability.stableLevyMeasure_abs_gt_pos {α β ε : ℝ} (hα : α ∈ Set.Ioo 0 2) (hβ : |β| ≤ 1) (hε : 0 < ε) : 0 < (stableLevyMeasure α β) {x : ℝ | ε < |x|}

The cutoff Lévy measure has positive mass, even at either full-skewness boundary.

theorem TauCeti.Probability.stableLevyMeasure_smallJumpBand_pos {α β ε r : ℝ} (hα : α ∈ Set.Ioo 0 2) (hβ : |β| ≤ 1) (hε : 0 < ε) (hεr : ε < r) : 0 < (stableLevyMeasure α β) {x : ℝ | ε < |x| ∧ |x| ≤ r}

A nonempty stable jump band has positive Lévy mass.

theorem TauCeti.Probability.stableLevyMeasure_abs_gt_ne_top {α β ε : ℝ} (hε : 0 < ε) : (stableLevyMeasure α β) {x : ℝ | ε < |x|} ≠ ⊤

The cutoff Lévy measure has finite mass for all parameters.

theorem TauCeti.Probability.isFiniteMeasure_stableLevyMeasure_restrict_abs_gt {α β ε : ℝ} (hε : 0 < ε) : MeasureTheory.IsFiniteMeasure ((stableLevyMeasure α β).restrict {x : ℝ | ε < |x|})

Restricting the stable Lévy measure away from zero gives a finite measure for all parameters.

theorem TauCeti.Probability.isProbabilityMeasure_cond_stableLevyMeasure {α β ε : ℝ} (hα : α ∈ Set.Ioo 0 2) (hβ : |β| ≤ 1) (hε : 0 < ε) : MeasureTheory.IsProbabilityMeasure (stableLevyMeasure α β)[|{x : ℝ | ε < |x|}]

Normalizing jumps larger than a positive cutoff gives a probability jump law.

theorem TauCeti.Probability.map_abs_restrict_stableLevyMeasure {α β ε : ℝ} (hα : α ∈ Set.Ioo 0 2) (hβ : |β| ≤ 1) (hε : 0 < ε) : MeasureTheory.Measure.map abs ((stableLevyMeasure α β).restrict {x : ℝ | ε < |x|}) = (stableLevyMeasure α β) {x : ℝ | ε < |x|} • ProbabilityTheory.paretoMeasure ε α

The absolute-value pushforward of the large-jump intensity is a multiple of a Pareto law. Its mass includes both tails, even when one of them vanishes at full skewness.

@[simp]

theorem TauCeti.Probability.map_abs_cond_stableLevyMeasure {α β ε : ℝ} (hα : α ∈ Set.Ioo 0 2) (hβ : |β| ≤ 1) (hε : 0 < ε) : MeasureTheory.Measure.map abs (stableLevyMeasure α β)[|{x : ℝ | ε < |x|}] = ProbabilityTheory.paretoMeasure ε α

The size of a stable Lévy jump conditioned to exceed a positive cutoff is Pareto, independently of the skewness parameter.

theorem TauCeti.Probability.isProbabilityMeasure_cond_stableLevyMeasure_smallJumpBand {α β ε r : ℝ} (hα : α ∈ Set.Ioo 0 2) (hβ : |β| ≤ 1) (hε : 0 < ε) (hεr : ε < r) : MeasureTheory.IsProbabilityMeasure (stableLevyMeasure α β)[|{x : ℝ | ε < |x| ∧ |x| ≤ r}]

For valid parameters, every nonempty stable jump band gives a probability jump law.

theorem TauCeti.Probability.integrable_stableLevyDensity_smul_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (α β : ℝ) {g : ℝ → E} : MeasureTheory.Integrable g (stableLevyMeasure α β) ↔ MeasureTheory.Integrable (fun (x : ℝ) => stableLevyDensity α β x • g x) MeasureTheory.volume

The density of a stable Lévy measure turns integrable functions into Lebesgue-integrable ones.

theorem TauCeti.Probability.integral_stableLevyMeasure_eq {α β : ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (hα : α ∈ Set.Ioo 0 2) (hβ : |β| ≤ 1) {g : ℝ → E} (hg : MeasureTheory.Integrable g (stableLevyMeasure α β)) : ∫ (x : ℝ), g x ∂stableLevyMeasure α β = ((Real.Gamma (1 + α) * Real.sin (Real.pi * α / 2) / Real.pi * (1 + β)) • ∫ (x : ℝ) in Set.Ioi 0, x ^ (-(α + 1)) • g x) + (Real.Gamma (1 + α) * Real.sin (Real.pi * α / 2) / Real.pi * (1 - β)) • ∫ (x : ℝ) in Set.Ioi 0, x ^ (-(α + 1)) • g (-x)

Integrals against a stable Lévy measure split into power-weighted integrals over the two half-lines.