Integrability of the compensated stable characteristic kernel

For non-Gaussian stable parameters, the Lévy measure has infinite mass near zero. Its second moment on a bounded neighbourhood of zero is nevertheless finite. Consequently the compensation exp (t * x * I) - 1 - t * sin x * I is absolutely integrable: it vanishes quadratically at zero and is bounded outside a neighbourhood of zero. The same argument applies along any unit complex direction u in place of I once the exponential term is essentially bounded, which covers the real kernel exp (t * x) - 1 - t * sin x on a half-line carrying the Lévy measure. The cutoff integrals converge to this integral, which is the analytic input to compensated compound Poisson approximations.

References

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

theorem TauCeti.Probability.integrable_cexp_mul_sub_one_sub_mul_sin_mul_stableLevyMeasure {α β t C : ℝ} {u : ℂ} (hu : ‖u‖ = 1) (hexp : ∀ᵐ (x : ℝ) ∂stableLevyMeasure α β, ‖Complex.exp (↑(t * x) * u)‖ ≤ C) : MeasureTheory.Integrable (fun (x : ℝ) => Complex.exp (↑(t * x) * u) - 1 - ↑(t * Real.sin x) * u) (stableLevyMeasure α β)

Along a unit complex direction u, the sine-compensated exponential kernel exp (t * x * u) - 1 - t * sin x * u is absolutely integrable against the stable Lévy measure whenever its exponential term is essentially bounded. The direction u = I gives the characteristic kernel and u = 1 the real exponential kernel.

theorem TauCeti.Probability.integrable_exp_sub_one_sub_sin_stableLevyMeasure (α β t : ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => Complex.exp (↑(t * x) * Complex.I) - 1 - ↑(t * Real.sin x) * Complex.I) (stableLevyMeasure α β)

The sine-compensated characteristic kernel is absolutely integrable against the stable Lévy measure, including at shape one and both full-skewness boundaries.

theorem TauCeti.Probability.integrable_exp_mul_sub_one_sub_mul_sin_stableLevyMeasure {α β t : ℝ} (ht : ∀ᵐ (x : ℝ) ∂stableLevyMeasure α β, t * x ≤ 0) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (t * x) - 1 - t * Real.sin x) (stableLevyMeasure α β)

If t * x ≤ 0 for almost every jump x of the stable Lévy measure, then the real compensated kernel exp (t * x) - 1 - t * sin x is integrable against the Lévy measure.

theorem TauCeti.Probability.tendsto_integral_exp_sub_one_sub_sin_stableLevyMeasure (α β t : ℝ) : Filter.Tendsto (fun (ε : ℝ) => ∫ (x : ℝ) in {x : ℝ | ε < |x|}, Complex.exp (↑(t * x) * Complex.I) - 1 - ↑(t * Real.sin x) * Complex.I ∂stableLevyMeasure α β) (nhds 0) (nhds (∫ (x : ℝ), Complex.exp (↑(t * x) * Complex.I) - 1 - ↑(t * Real.sin x) * Complex.I ∂stableLevyMeasure α β))

Removing a shrinking neighbourhood of zero from the compensated integral recovers the full integral. No one-sided restriction on the cutoff is needed.

theorem TauCeti.Probability.tendsto_integral_exp_mul_sub_one_sub_mul_sin_stableLevyMeasure {α β t : ℝ} (ht : ∀ᵐ (x : ℝ) ∂stableLevyMeasure α β, t * x ≤ 0) : Filter.Tendsto (fun (ε : ℝ) => ∫ (x : ℝ) in {x : ℝ | ε < |x|}, Real.exp (t * x) - 1 - t * Real.sin x ∂stableLevyMeasure α β) (nhds 0) (nhds (∫ (x : ℝ), Real.exp (t * x) - 1 - t * Real.sin x ∂stableLevyMeasure α β))

If t * x ≤ 0 for almost every jump, removing a shrinking neighbourhood of zero recovers the real compensated Lévy integral. No one-sided restriction on the cutoff is needed.