Stable distributions and domains of attraction

12 fully proved

Convolution powers

TheoremConvolution powers of a Gaussian are Gaussian#✓fully proved

The convolution power of a Gaussian is Gaussian with the mean and the variance multiplied by n: the law of the sum of n i.i.d. N(μ, v) variables is N(nμ, nv).

theorem convPow_gaussianReal (μ : ℝ) (v : ℝ≥0) (n : ℕ) :
    Measure.convPow (gaussianReal μ v) n =
      gaussianReal ((n : ℝ) * μ) ((n : ℝ≥0) * v)

Uses 2 · Used by 2

Statement usesConvolution power of a measure

Proof usesRecursion for convolution powers

Used byGaussian measures are stable of index 2 · Nondegenerate Gaussian is not stable of index 1

Stable laws

DefinitionStable distribution of a given index#✓fully proved

Indexed stability fixes the positive-n dilation to n^(1/α) and allows arbitrary centering. Degenerate Dirac identities may satisfy several indices.

def IsStable (μ : Measure ℝ) (α : ℝ) : Prop :=
  IsProbabilityMeasure μ ∧ 0 < α ∧ α ≤ 2 ∧
  ∀ n : ℕ, 0 < n → ∃ b : ℝ,
    μ.convPow n = μ.map (fun x => (n : ℝ) ^ (1 / α) * x + b)

Uses 1 · Used by 5

Statement usesConvolution power of a measure

Used byDomain of attraction of a given index · Stable law lies in its own domain of attraction · Dirac measures are stable of every index · Gaussian measures are stable of index 2 · Nondegenerate Gaussian is not stable of index 1

TheoremDirac measures are stable of every index#✓fully proved

A Dirac law satisfies the fixed-dilation identity at every admissible index. These are degenerate rescaling identities, with centering na - n^(1/α)a.

theorem isStable_dirac (a : ℝ) {α : ℝ} (hα0 : 0 < α) (hα2 : α ≤ 2) :
    IsStable (dirac a) α

Uses 3

Statement usesStable distribution of a given index

Proof usesConvolution power of a measure · Convolution powers of a Dirac measure

TheoremGaussian measures are stable of index 2#✓fully proved

Every real Gaussian measure is stable of index 2: the sum of n i.i.d. N(μ, v) variables is N(nμ, nv), which is the pushforward of N(μ, v) under x ↦ √n · x + (n - √n) μ.

theorem isStable_gaussianReal (μ : ℝ) (v : ℝ≥0) :
    IsStable (gaussianReal μ v) 2

Uses 3

Statement usesStable distribution of a given index

Proof usesConvolution powers of a Gaussian are Gaussian · Convolution power of a measure

TheoremNondegenerate Gaussian is not stable of index 1#✓fully proved

A nondegenerate Gaussian cannot have fixed stability index one. The n=4 convolution variance is 4v, while every such affine dilation has variance 16v.

theorem not_isStable_gaussianReal_one {μ : ℝ} {v : ℝ≥0} (hv : v ≠ 0) :
    ¬ IsStable (gaussianReal μ v) 1

Uses 3

Statement usesStable distribution of a given index

Proof usesConvolution powers of a Gaussian are Gaussian · Convolution power of a measure

DefinitionNondegenerate measure on the real line#✓fully proved

A measure μ on ℝ is nondegenerate if it is not a point mass δ_a for any a.

def IsNondegenerate (μ : Measure ℝ) : Prop :=
  ¬ ∃ a : ℝ, μ = Measure.dirac a

Used by 3

Used byDomain of attraction of a given index · Gaussian with nonzero variance is nondegenerate · Dirac measure is degenerate

TheoremGaussian with nonzero variance is nondegenerate#✓fully proved

A Gaussian with nonzero variance is nondegenerate: it gives mass 0 to every singleton, while δ_a gives mass 1 to {a}.

theorem isNondegenerate_gaussianReal {μ : ℝ} {v : ℝ≥0} (hv : v ≠ 0) :
    IsNondegenerate (gaussianReal μ v)

Uses 1

Statement usesNondegenerate measure on the real line

TheoremDirac measure is degenerate#✓fully proved

A Dirac measure is degenerate, by definition.

theorem not_isNondegenerate_dirac (a : ℝ) :
    ¬ IsNondegenerate (Measure.dirac a)

Uses 1

Statement usesNondegenerate measure on the real line

Domains of attraction

DefinitionDomain of attraction#✓fully proved

The probability measure μ is in the domain of attraction of G if there exist sequences of normalizing constants a n > 0 and centering constants b n such that the law of (S_n - b n) / a n (where S_n has law μ^{*n}) converges weakly to G, expressed here as integration against arbitrary bounded continuous functions.

def InDomainOfAttraction (μ G : Measure ℝ) : Prop :=
  IsProbabilityMeasure μ ∧ IsProbabilityMeasure G ∧
  ∃ (a : ℕ → ℝ) (b : ℕ → ℝ),
    (∀ n, 0 < a n) ∧
    ∀ (f : ℝ →ᵇ ℝ),
      Tendsto
        (fun n => ∫ x, f x ∂(Measure.map (fun y => (y - b n) / a n)
          (Measure.convPow μ n)))
        atTop (𝓝 (∫ x, f x ∂G))

Uses 1 · Used by 3

Statement usesConvolution power of a measure

Used byDirac measure lies in its own domain of attraction · Domain of attraction of a given index · Stable law lies in its own domain of attraction

TheoremStable law lies in its own domain of attraction#✓fully proved

A stable law is a normalized weak limit of its own convolution powers. The positive-n inverse affine identity is exact; order zero uses normalizer one.

theorem IsStable.inDomainOfAttraction_self {μ : Measure ℝ} {α : ℝ}
    (h : IsStable μ α) : InDomainOfAttraction μ μ

Uses 3

Statement usesDomain of attraction · Stable distribution of a given index

Proof usesConvolution power of a measure

DefinitionDomain of attraction of a given index#✓fully proved

Indexed attraction requires a nondegenerate stable limit of that index. The general normalized weak-limit relation alone does not assign an index.

def InDomainOfAttractionIndex (μ : Measure ℝ) (α : ℝ) : Prop :=
  ∃ G : Measure ℝ, IsStable G α ∧ IsNondegenerate G ∧ InDomainOfAttraction μ G

Uses 3

Statement usesDomain of attraction · Nondegenerate measure on the real line · Stable distribution of a given index

TheoremDirac measure lies in its own domain of attraction#✓fully proved

The Dirac measure is in its own domain of attraction: with a n = 1 and b n = (n - 1) a, the normalized law of S_n is δ_a for every n.

theorem inDomainOfAttraction_dirac (a : ℝ) :
    InDomainOfAttraction (Measure.dirac a) (Measure.dirac a)

Uses 3

Statement usesDomain of attraction

Proof usesConvolution power of a measure · Convolution powers of a Dirac measure

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.