noncomputable def MeasureTheory.Measure.convPow {M : Type u_1} [AddCommMonoid M] [MeasurableSpace M] (ν : Measure M) : ℕ → Measure M

The n-fold convolution power of a measure ν on an additive commutative measurable monoid. Defined recursively: convPow ν 0 = δ_0 (Dirac at the additive identity) and convPow ν (n+1) = convPow ν n ∗ ν. If ν is the law of Y, then convPow ν n is the law of the sum of n i.i.d. copies of Y.

def IsInfinitelyDivisible {M : Type u_1} [AddCommMonoid M] [MeasurableSpace M] (μ : MeasureTheory.Measure M) : Prop

A measure μ on an additive commutative measurable monoid is infinitely divisible if for every n ≥ 1 there is a probability measure ν whose n-fold convolution power equals μ. Equivalently, the corresponding random variable X can, for every n, be written in law as the sum of n i.i.d. copies of some random variable Y.