The unconditional stable law and its convolution semigroup

This module packages the scalar stable density as a probability measure for every 1 < θ ≤ 2, identifies its Laplace and characteristic transforms, and proves the time semigroup for the corresponding laws and densities.

References: V. M. Zolotarev, One-dimensional Stable Distributions, 1986; K. Sato, Lévy Processes and Infinitely Divisible Distributions, 1999, §14; W. Feller, An Introduction to Probability Theory and Its Applications, vol. II, ch. XVII.

theorem BGW.StableTrees.exists_stableDomain {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∃ (μ : PMF ℕ) (a : ℕ → ℝ), StableDomain μ θ a

For every index 1 < θ ≤ 2, some critical offspring law lies in the normalized θ-stable domain of attraction (C15.1; witness by an explicit regularly varying tail).

theorem BGW.StableTrees.stableDensity_nonneg {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : ℝ) : 0 ≤ Scalar.stableDensity θ x

The stable density is nonnegative, unconditionally on 1 < θ ≤ 2 (C15.1).

theorem BGW.StableTrees.integral_stableDensity {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∫ (x : ℝ), Scalar.stableDensity θ x = 1

The stable density integrates to one (C15.1).

noncomputable def BGW.StableTrees.stableLaw (θ : ℝ) : MeasureTheory.ProbabilityMeasure ℝ

The spectrally positive θ-stable law, normalized by E[exp(-λ X)] = exp(λ^θ), for 1 < θ ≤ 2; the Dirac mass at 0 outside this range (a junk value).

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.StableTrees.stableLaw_eq_withDensity {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ↑(stableLaw θ) = MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (Scalar.stableDensity θ x)

The stable law has density Scalar.stableDensity θ (C15.1).

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

Laplace transform of the stable law (C15.1).

theorem BGW.StableTrees.charFun_stableLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : ℝ) : MeasureTheory.charFun (↑(stableLaw θ)) t = Scalar.stableCF θ t

Characteristic function of the stable law: exp ((-i t)^θ) (C15.1).

theorem BGW.StableTrees.eq_stableLaw_of_laplace {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure ν] (hL : ∀ (lam : ℝ), 0 < lam → ∫ (y : ℝ), Real.exp (-lam * y) ∂ν = Real.exp (lam ^ θ)) : ν = ↑(stableLaw θ)

The stable law is the only probability measure with this Laplace transform (C15.1).

theorem BGW.StableTrees.stableLaw_two : ↑(stableLaw 2) = ProbabilityTheory.gaussianReal 0 2

At θ = 2 the stable law is the centered Gaussian of variance 2 (C15; §1.1).

noncomputable def BGW.StableTrees.stableDensityAt (θ t x : ℝ) : ℝ

The density of the stable law at time t > 0: t^{-1/θ} p₁(t^{-1/θ} x) (C15.4).

Equations

• BGW.StableTrees.stableDensityAt θ t x = t ^ (-1 / θ) * BGW.StableTrees.Scalar.stableDensity θ (t ^ (-1 / θ) * x)

noncomputable def BGW.StableTrees.stableLawAt (θ t : ℝ) : MeasureTheory.ProbabilityMeasure ℝ

The stable law at time t > 0, image of stableLaw θ under x ↦ t^{1/θ} x (C15.4).

Equations

• BGW.StableTrees.stableLawAt θ t = (BGW.StableTrees.stableLaw θ).map fun (x : ℝ) => t ^ (1 / θ) * x

theorem BGW.StableTrees.stableLawAt_eq_withDensity {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : ℝ} (ht : 0 < t) : ↑(stableLawAt θ t) = MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (stableDensityAt θ t x)

stableLawAt θ t has density stableDensityAt θ t (C15.4).

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

Laplace transform at time t: E[exp(-λ X_t)] = exp(t λ^θ) (C15.4).

theorem BGW.StableTrees.stableLawAt_conv {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {s t : ℝ} (hs : 0 < s) (ht : 0 < t) : (↑(stableLawAt θ s)).conv ↑(stableLawAt θ t) = ↑(stableLawAt θ (s + t))

Semigroup property of the stable laws (C15.4).

theorem BGW.StableTrees.integral_stableDensityAt_mul {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {s t : ℝ} (hs : 0 < s) (ht : 0 < t) (x : ℝ) : ∫ (y : ℝ), stableDensityAt θ s y * stableDensityAt θ t (x - y) = stableDensityAt θ (s + t) x

Semigroup property of the stable densities: p_s * p_t = p_{s+t} (C15.4).