Infinitely divisible distributions

DefinitionConvolution power of a measure#✓fully proved

Let \(M\) be an additive commutative monoid with a σ-algebra and let \(\nu\) be a measure on \(M\). The \(n\)-th convolution power \(\nu^{*n}\) of \(\nu\) is defined by recursion on \(n\): \(\nu^{*0} = \delta_0\), the Dirac measure at the identity \(0\) of \(M\), and \(\nu^{*(n+1)} = \nu^{*n} * \nu\), where \(*\) denotes convolution of measures.

When addition on \(M\) is jointly measurable and \(\nu\) is the law of a random variable \(Y\), \(\nu^{*n}\) is the law of the sum of \(n\) independent copies of \(Y\).

noncomputable def convPow {M : Type*} [AddCommMonoid M] [MeasurableSpace M]
    (ν : Measure M) : ℕ → Measure M
  | 0 => dirac 0
  | n + 1 => (ν.convPow n) ∗ ν

Used by 29

Used byGeneration-size law of a Galton–Watson process · Mean generation size of a Galton–Watson process · Generating function of the n-th generation size · Extinction by generation n converges to the extinction probability · Infinite divisibility is closed under convolution · Convolution powers add exponents · Convolution power of a convolution · Convolution powers of a Dirac measure · The first convolution power · Recursion for convolution powers · Convolution powers as iterated left convolution · Convolution powers of a Poisson measure · The zeroth convolution power · Infinitely divisible measures · Dirac measures on the real line are infinitely divisible · Infinite divisibility through iterated convolution · Poisson distributions are infinitely divisible · Infinitely divisible measures are probability measures · Convolution powers of a probability measure are probability measures · Convolution powers of an s-finite measure are s-finite · Lévy–Khintchin representation on the real line · Convolution powers of a Gaussian are Gaussian · Domain of attraction · Dirac measure lies in its own domain of attraction · Stable law lies in its own domain of attraction · Stable distribution of a given index · Dirac measures are stable of every index · Gaussian measures are stable of index 2 · Nondegenerate Gaussian is not stable of index 1

TheoremThe zeroth convolution power#✓fully proved

For every measure \(\nu\) on an additive commutative monoid \(M\) with a σ-algebra, the zeroth convolution power of \(\nu\) is the Dirac measure \(\delta_0\) at the identity element \(0\) of \(M\).

theorem convPow_zero (ν : Measure M) : convPow ν 0 = dirac 0

Uses 1 · Used by 5

Statement usesConvolution power of a measure

Used byConvolution powers add exponents · Convolution powers of a Dirac measure · The first convolution power · Convolution powers of a probability measure are probability measures · Convolution powers of an s-finite measure are s-finite

TheoremRecursion for convolution powers#✓fully proved

Let \(M\) be an additive commutative monoid with a σ-algebra and let \(\nu\) be a measure on \(M\). For every natural number \(n\), the \((n+1)\)-st convolution power of \(\nu\) is the convolution of the \(n\)-th convolution power of \(\nu\) with \(\nu\).

theorem convPow_succ (ν : Measure M) (n : ℕ) : convPow ν (n + 1) = convPow ν n ∗ ν

Uses 1 · Used by 11

Statement usesConvolution power of a measure

Used byMean generation size of a Galton–Watson process · Generating function of the n-th generation size · Convolution powers add exponents · Convolution power of a convolution · Convolution powers of a Dirac measure · The first convolution power · Convolution powers as iterated left convolution · Convolution powers of a Poisson measure · Convolution powers of a probability measure are probability measures · Convolution powers of an s-finite measure are s-finite · Convolution powers of a Gaussian are Gaussian

TheoremThe first convolution power#✓fully proved

Let \(M\) be an additive commutative monoid with a σ-algebra for which addition \(M \times M \to M\) is measurable, and let \(\nu\) be an s-finite measure on \(M\). Then the first convolution power of \(\nu\) is \(\nu\) itself.

theorem convPow_one [MeasurableAdd₂ M] {ν : Measure M} [SFinite ν] :
    convPow ν 1 = ν

Uses 3 · Used by 3

Statement usesConvolution power of a measure

Proof usesRecursion for convolution powers · The zeroth convolution power

Used byConvolution powers as iterated left convolution · Convolution powers of a Poisson measure · Infinitely divisible measures are probability measures

TheoremConvolution powers of an s-finite measure are s-finite#✓fully proved

Let \(M\) be an additive commutative monoid with a measurable structure. If \(\nu\) is an s-finite measure on \(M\), then for every natural number \(n\) its \(n\)-fold convolution power \(\nu^{*n}\) is s-finite.

theorem sfinite_convPow {ν : Measure M} [SFinite ν] (n : ℕ) : SFinite (convPow ν n)

Uses 3 · Used by 3

Statement usesConvolution power of a measure

Proof usesRecursion for convolution powers · The zeroth convolution power

Used byConvolution powers add exponents · Convolution power of a convolution · Convolution powers as iterated left convolution

TheoremConvolution powers of a probability measure are probability measures#✓fully proved

Let \(M\) be an additive commutative monoid with a measurable structure. If \(\nu\) is a probability measure on \(M\), then for every natural number \(n\) its \(n\)-fold convolution power \(\nu^{*n}\) is a probability measure.

theorem isProbabilityMeasure_convPow {ν : Measure M} [IsProbabilityMeasure ν] (n : ℕ) :
    IsProbabilityMeasure (convPow ν n)

Uses 3 · Used by 4

Statement usesConvolution power of a measure

Proof usesRecursion for convolution powers · The zeroth convolution power

Used byMean generation size of a Galton–Watson process · Generating function of the n-th generation size · Extinction by generation n converges to the extinction probability · Lévy–Khintchin representation on the real line

TheoremConvolution powers as iterated left convolution#✓fully proved

Let \(M\) be an additive commutative monoid with a σ-algebra for which addition \(M \times M \to M\) is measurable, and let \(\nu\) be an s-finite measure on \(M\). For every natural number \(n\), the \((n+1)\)-st convolution power of \(\nu\) equals the measure obtained from \(\nu\) by applying the map \(\mu \mapsto \nu * \mu\) exactly \(n\) times, where \(*\) denotes convolution of measures.

theorem convPow_succ_eq_iterate [MeasurableAdd₂ M] {ν : Measure M} [SFinite ν] (n : ℕ) :
    convPow ν (n + 1) = Nat.iterate (Measure.conv ν) n ν

Uses 4 · Used by 2

Statement usesConvolution power of a measure

Proof usesThe first convolution power · Recursion for convolution powers · Convolution powers of an s-finite measure are s-finite

Used byInfinite divisibility through iterated convolution · Lévy–Khintchin representation on the real line

TheoremConvolution powers add exponents#✓fully proved

Let \(M\) be an additive commutative monoid with a σ-algebra for which addition \(M \times M \to M\) is measurable, and let \(\nu\) be an s-finite measure on \(M\). Writing \(*\) for convolution of measures and \(\nu^{*n}\) for the \(n\)-th convolution power of \(\nu\), for all natural numbers \(m\) and \(n\) we have \(\nu^{*(m+n)} = \nu^{*m} * \nu^{*n}\).

theorem convPow_add [MeasurableAdd₂ M] {ν : Measure M} [SFinite ν] (m n : ℕ) :
    convPow ν (m + n) = convPow ν m ∗ convPow ν n

Uses 4

Statement usesConvolution power of a measure

Proof usesRecursion for convolution powers · The zeroth convolution power · Convolution powers of an s-finite measure are s-finite

TheoremInterchange law for convolution#✓fully proved

Let \(M\) be an additive commutative monoid with a σ-algebra for which addition \(M \times M \to M\) is measurable. For all s-finite measures \(a, b, c, d\) on \(M\) we have \((a * b) * (c * d) = (a * c) * (b * d)\), where \(*\) denotes convolution of measures.

theorem conv_mul_conv [MeasurableAdd₂ M] {a b c d : Measure M}
    [SFinite a] [SFinite b] [SFinite c] [SFinite d] :
    (a ∗ b) ∗ (c ∗ d) = (a ∗ c) ∗ (b ∗ d)

Used by 1

Used byConvolution power of a convolution

TheoremConvolution power of a convolution#✓fully proved

Let \(M\) be an additive commutative monoid with a σ-algebra for which addition \(M \times M \to M\) is measurable, and let \(\nu\) and \(\rho\) be s-finite measures on \(M\). Writing \(*\) for convolution of measures and \(\mu^{*n}\) for the \(n\)-th convolution power of a measure \(\mu\), for every natural number \(n\) we have \((\nu * \rho)^{*n} = \nu^{*n} * \rho^{*n}\).

theorem convPow_conv [MeasurableAdd₂ M] {ν ρ : Measure M} [SFinite ν] [SFinite ρ] (n : ℕ) :
    convPow (ν ∗ ρ) n = convPow ν n ∗ convPow ρ n

Uses 4 · Used by 1

Statement usesConvolution power of a measure

Proof usesRecursion for convolution powers · Interchange law for convolution · Convolution powers of an s-finite measure are s-finite

Used byInfinite divisibility is closed under convolution

DefinitionInfinitely divisible measures#✓fully proved

Let \(M\) be an additive commutative monoid with a measurable structure in which addition is jointly measurable. A measure \(\mu\) on \(M\) is infinitely divisible if for every natural number \(n \ge 1\) there is a probability measure \(\nu\) on \(M\) whose \(n\)-fold convolution power \(\nu^{*n}\) equals \(\mu\).

Equivalently, a random variable \(X\) with law \(\mu\) can, for every \(n \ge 1\), be written in law as the sum of \(n\) i.i.d. copies of some random variable \(Y\).

def IsInfinitelyDivisible {M : Type*} [AddCommMonoid M] [MeasurableSpace M]
    [MeasurableAdd₂ M]
    (μ : Measure M) : Prop :=
  ∀ n : ℕ, n ≥ 1 → ∃ ν : Measure M, IsProbabilityMeasure ν ∧ μ = ν.convPow n

Uses 1 · Used by 6

Statement usesConvolution power of a measure

Used byInfinite divisibility is closed under convolution · Dirac measures on the real line are infinitely divisible · Infinite divisibility through iterated convolution · Poisson distributions are infinitely divisible · Infinitely divisible measures are probability measures · Lévy–Khintchin representation on the real line

TheoremInfinitely divisible measures are probability measures#✓fully proved

Let \(M\) be an additive commutative monoid with a measurable structure in which addition is jointly measurable. Every infinitely divisible measure on \(M\) is a probability measure.

The convolution root of order one is the measure itself, and it is a probability measure by definition.

theorem IsInfinitelyDivisible.isProbabilityMeasure [MeasurableAdd₂ M] {μ : Measure M}
    (hμ : IsInfinitelyDivisible μ) : IsProbabilityMeasure μ

Uses 3

Statement usesInfinitely divisible measures

Proof usesConvolution power of a measure · The first convolution power

TheoremInfinite divisibility through iterated convolution#✓fully proved

Let \(M\) be an additive commutative monoid with a measurable structure in which addition is jointly measurable. A measure \(\mu\) on \(M\) is infinitely divisible if and only if for every natural number \(n \ne 0\) there is a probability measure \(\nu\) on \(M\) such that \(\mu = \nu * (\nu * (\cdots * (\nu * \nu)))\) with \(n\) factors \(\nu\), that is, \(\mu\) is obtained from \(\nu\) by convolving on the left with \(\nu\) exactly \(n - 1\) times.

theorem isInfinitelyDivisible_iff_exists_iterate [MeasurableAdd₂ M] (μ : Measure M) :
    IsInfinitelyDivisible μ ↔
      ∀ n : ℕ, n ≠ 0 → ∃ ν : Measure M, IsProbabilityMeasure ν ∧
        μ = Nat.iterate (Measure.conv ν) (n - 1) ν

Uses 3 · Used by 1

Statement usesInfinitely divisible measures

Proof usesConvolution power of a measure · Convolution powers as iterated left convolution

Used byLévy–Khintchin representation on the real line

TheoremInfinite divisibility is closed under convolution#✓fully proved

Let \(M\) be an additive commutative monoid with a measurable structure in which addition is jointly measurable. If \(\mu\) and \(\eta\) are infinitely divisible measures on \(M\), then their convolution \(\mu * \eta\) is infinitely divisible.

For each \(n \ge 1\), convolving an \(n\)-th convolution root of \(\mu\) with one of \(\eta\) gives an \(n\)-th convolution root of \(\mu * \eta\).

theorem IsInfinitelyDivisible.conv [MeasurableAdd₂ M] {μ η : Measure M}
    (hμ : IsInfinitelyDivisible μ) (hη : IsInfinitelyDivisible η) :
    IsInfinitelyDivisible (μ ∗ η)

Uses 3

Statement usesInfinitely divisible measures

Proof usesConvolution power of a measure · Convolution power of a convolution

TheoremConvolution powers of a Dirac measure#✓fully proved

Let \(M\) be an additive commutative monoid with a σ-algebra for which addition \(M \times M \to M\) is measurable. For every point \(x \in M\) and every natural number \(n\), the \(n\)-th convolution power of the Dirac measure \(\delta_x\) is \(\delta_{nx}\), where \(nx\) is the sum of \(n\) copies of \(x\) (so \(0x = 0\)).

theorem convPow_dirac [MeasurableAdd₂ M] (x : M) (n : ℕ) :
    convPow (dirac x) n = dirac (n • x)

Uses 3 · Used by 3

Statement usesConvolution power of a measure

Proof usesRecursion for convolution powers · The zeroth convolution power

Used byDirac measures on the real line are infinitely divisible · Dirac measure lies in its own domain of attraction · Dirac measures are stable of every index

TheoremDirac measures on the real line are infinitely divisible#✓fully proved

For every real number \(a\), the Dirac measure \(\delta_a\) on \(\mathbb{R}\) is infinitely divisible: for every \(n \ge 1\), \(\delta_a\) is the \(n\)-fold convolution power of \(\delta_{a/n}\).

theorem isInfinitelyDivisible_dirac (a : ℝ) :
    IsInfinitelyDivisible (dirac a)

Uses 3

Statement usesInfinitely divisible measures

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

TheoremConvolution powers of a Poisson measure#✓fully proved

For every real rate \(r \ge 0\) and every natural number \(n\), the \((n+1)\)-st convolution power of the Poisson measure on \(\mathbb{N}\) with rate \(r\) is the Poisson measure on \(\mathbb{N}\) with rate \((n+1)r\).

theorem convPow_succ_poissonMeasure (r : ℝ≥0) (n : ℕ) :
    convPow (ProbabilityTheory.poissonMeasure r) (n + 1) =
      ProbabilityTheory.poissonMeasure ((n + 1) • r)

Uses 3 · Used by 1

Statement usesConvolution power of a measure

Proof usesThe first convolution power · Recursion for convolution powers

Used byPoisson distributions are infinitely divisible

TheoremPoisson distributions are infinitely divisible#✓fully proved

For every real \(r \ge 0\), the Poisson distribution with parameter \(r\), as a measure on \(\mathbb{N}\), is infinitely divisible: for every \(n \ge 1\) it is the \(n\)-fold convolution power of the Poisson distribution with parameter \(r/n\).

theorem isInfinitelyDivisible_poissonMeasure (r : ℝ≥0) :
    IsInfinitelyDivisible (ProbabilityTheory.poissonMeasure r)

Uses 3

Statement usesInfinitely divisible measures

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

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.