Characteristic exponents of scalar stable laws

This file defines the characteristic exponent of a scalar stable law in Nolan's S₀ parameterization. This convention is continuous through shape one: away from shape one the imaginary part contains sign u * |u| ^ α - u, while at shape one its limiting logarithmic term is used explicitly.

continuous_stableCharacteristicExponent_params proves this parameter continuity at every fixed frequency, using Mathlib's dslope to remove the shape-one singularity.

The exponent has real part -|u| ^ α, is compatible with reflection and complex conjugation, and is continuous at the origin for every positive shape. Its exponential therefore has modulus exp (-|u| ^ α). The Gaussian and symmetric Cauchy exponents occur at shapes two and one.

stableS1Location records the location parameter in Nolan's S₁ convention. The final two identities give the corresponding S₁ characteristic exponent without introducing a second family of stable measures.

References

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

noncomputable def TauCeti.Probability.stableCharacteristicExponent (α β u : ℝ) : ℂ

The characteristic exponent of a standardized scalar stable law in Nolan's S₀ parameterization. Its value at zero is specified separately from the two displayed formulas.

@[simp]

theorem TauCeti.Probability.stableCharacteristicExponent_zero (α β : ℝ) : stableCharacteristicExponent α β 0 = 0

theorem TauCeti.Probability.stableCharacteristicExponent_one (β u : ℝ) : stableCharacteristicExponent 1 β u = -↑|u| - ↑(2 * β / Real.pi * u * Real.log |u|) * Complex.I

The logarithmic shape-one branch.

theorem TauCeti.Probability.stableCharacteristicExponent_of_ne_one_of_ne_zero {α : ℝ} (hα : α ≠ 1) (β : ℝ) {u : ℝ} (hu : u ≠ 0) : stableCharacteristicExponent α β u = ↑(-|u| ^ α) + ↑(β * Real.tan (Real.pi * α / 2) * (u.sign * |u| ^ α - u)) * Complex.I

The non-logarithmic branch away from shape one and the origin.

@[simp]

theorem TauCeti.Probability.stableCharacteristicExponent_re {α : ℝ} (hα : α ≠ 0) (β u : ℝ) : (stableCharacteristicExponent α β u).re = -|u| ^ α

The real part of the stable exponent is the negative stable power.

theorem TauCeti.Probability.stableCharacteristicExponent_neg (α β u : ℝ) : stableCharacteristicExponent α β (-u) = (starRingEnd ℂ) (stableCharacteristicExponent α β u)

Reflection of the argument is complex conjugation of the exponent.

theorem TauCeti.Probability.stableCharacteristicExponent_neg_skew (α β u : ℝ) : stableCharacteristicExponent α (-β) u = stableCharacteristicExponent α β (-u)

Negating the skewness parameter has the same effect as reflecting the argument.

theorem TauCeti.Probability.stableCharacteristicExponent_mul (α β b u : ℝ) : stableCharacteristicExponent α β (b * u) = stableCharacteristicExponent α (b.sign * β) (|b| * u)

Scaling the argument by b is scaling by |b| with the skewness multiplied by the sign of b. At b = 0 both sides are the value zero at the origin.

theorem TauCeti.Probability.stableCharacteristicExponent_im_eq_mul (α β u : ℝ) : (stableCharacteristicExponent α β u).im = β * (stableCharacteristicExponent α 1 u).im

The imaginary part of the stable exponent is linear in the skewness parameter: it is β times the imaginary part of the totally skewed exponent.

theorem TauCeti.Probability.stableCharacteristicExponent_im_of_ne_one {α : ℝ} (hα : α ≠ 1) (β u : ℝ) : (stableCharacteristicExponent α β u).im = β * Real.tan (Real.pi * α / 2) * (u * |u| ^ (α - 1) - u)

Away from shape one, the imaginary part of the stable exponent is β tan (π α / 2) (u |u| ^ (α - 1) - u); this form also holds at the origin.

@[simp]

theorem TauCeti.Probability.stableCharacteristicExponent_two (β u : ℝ) : stableCharacteristicExponent 2 β u = -↑(u ^ 2)

At shape two the exponent is the centered Gaussian exponent -u², independently of skewness.

@[simp]

theorem TauCeti.Probability.stableCharacteristicExponent_one_zero (u : ℝ) : stableCharacteristicExponent 1 0 u = -↑|u|

At shape one and zero skewness the exponent is the centered Cauchy exponent.

@[simp]

theorem TauCeti.Probability.norm_exp_stableCharacteristicExponent {α : ℝ} (hα : α ≠ 0) (β u : ℝ) : ‖Complex.exp (stableCharacteristicExponent α β u)‖ = Real.exp (-|u| ^ α)

The modulus of the exponential of a stable exponent is exp (-|u| ^ α).

theorem TauCeti.Probability.continuousAt_stableCharacteristicExponent_zero {α : ℝ} (hα : 0 < α) (β : ℝ) : ContinuousAt (stableCharacteristicExponent α β) 0

For positive shape, the stable characteristic exponent is continuous at the origin.

theorem TauCeti.Probability.continuous_stableCharacteristicExponent_params (u : ℝ) : Continuous fun (p : ↑(Set.Ioc 0 2) × ℝ) => stableCharacteristicExponent (↑p.1) p.2 u

At each fixed frequency, the stable exponent depends continuously on shape and skewness throughout 0 < α ≤ 2. In particular, the logarithmic branch is the limit at shape one.

noncomputable def TauCeti.Probability.stableS1Location (α β : ℝ) (s : NNReal) (m : ℝ) : ℝ

The location in Nolan's S₁ parameterization corresponding to an S₀ location m.

@[simp]

theorem TauCeti.Probability.stableS1Location_zero_scale (α β m : ℝ) : stableS1Location α β 0 m = m

theorem TauCeti.Probability.stableS1Location_eq_add (α β : ℝ) (s : NNReal) (m : ℝ) : stableS1Location α β s m = m + stableS1Location α β s 0

The S₁ correction does not depend on the location: the S₁ location is the S₀ location plus the S₁ location of the same law centred at zero.

theorem TauCeti.Probability.stableS1Location_of_ne_one {α : ℝ} (hα : α ≠ 1) (β : ℝ) {s : NNReal} (m : ℝ) : stableS1Location α β s m = m - β * ↑s * Real.tan (Real.pi * α / 2)

The S₁ location correction away from shape one.

theorem TauCeti.Probability.stableS1Location_one (β : ℝ) {s : NNReal} (m : ℝ) : stableS1Location 1 β s m = m - 2 / Real.pi * β * ↑s * Real.log ↑s

The logarithmic S₁ location correction at shape one.

theorem TauCeti.Probability.stableCharacteristicExponent_add_location_eq_s1_of_ne_one {α : ℝ} (hα : α ≠ 1) (hα0 : α ≠ 0) (β : ℝ) (s : NNReal) (m t : ℝ) : ↑(m * t) * Complex.I + stableCharacteristicExponent α β (↑s * t) = ↑(-|↑s * t| ^ α) + ↑(stableS1Location α β s m * t + β * t.sign * |↑s * t| ^ α * Real.tan (Real.pi * α / 2)) * Complex.I

Away from shape one, adding an S₀ location to the stable exponent gives the usual S₁ exponent with the corrected location.

theorem TauCeti.Probability.stableCharacteristicExponent_add_location_eq_s1_one (β : ℝ) (s : NNReal) (m t : ℝ) : ↑(m * t) * Complex.I + stableCharacteristicExponent 1 β (↑s * t) = -↑|↑s * t| + ↑(stableS1Location 1 β s m * t - 2 / Real.pi * β * ↑s * t * Real.log |t|) * Complex.I

At shape one, adding an S₀ location to the stable exponent gives the logarithmic S₁ exponent with the corrected location.