Convolution powers of measures

This file defines the additive convolution powers of a measure on a measurable additive monoid. It records their algebraic, measure-theoretic, measurability, and integration properties, the distributivity of convolution over countable sums (conv_sum), the bound of the mass of Iic t under a convolution in a canonically ordered monoid (conv_Iic_le), the compatibility of mixtures of a convolution-additive family with convolution (bind_conv_bind), and the characteristic function of a convolution power (charFun_convolutionPower).

def MeasureTheory.Measure.convolutionPower {α : Type u_1} [MeasurableSpace α] [AddMonoid α] (μ : Measure α) : ℕ → Measure α

The n-fold additive convolution of a measure. The zeroth power is the point mass at zero.

@[simp]

theorem MeasureTheory.Measure.convolutionPower_zero {α : Type u_1} [MeasurableSpace α] [AddMonoid α] (μ : Measure α) : μ.convolutionPower 0 = dirac 0

The zeroth convolution power is the point mass at zero.

@[simp]

theorem MeasureTheory.Measure.convolutionPower_succ {α : Type u_1} [MeasurableSpace α] [AddMonoid α] (μ : Measure α) (n : ℕ) : μ.convolutionPower (n + 1) = (μ.convolutionPower n).conv μ

A successor convolution power appends one copy of the measure.

instance MeasureTheory.Measure.sfinite_convolutionPower {α : Type u_1} [MeasurableSpace α] [AddMonoid α] (μ : Measure α) [SFinite μ] (n : ℕ) : SFinite (μ.convolutionPower n)

Convolution powers of an s-finite measure are s-finite.

instance MeasureTheory.Measure.isFiniteMeasure_convolutionPower {α : Type u_1} [MeasurableSpace α] [AddMonoid α] (μ : Measure α) [IsFiniteMeasure μ] (n : ℕ) : IsFiniteMeasure (μ.convolutionPower n)

Convolution powers of a finite measure are finite.

theorem MeasureTheory.Measure.convolutionPower_one {α : Type u_1} [MeasurableSpace α] [AddMonoid α] [MeasurableAdd₂ α] (μ : Measure α) [SFinite μ] : μ.convolutionPower 1 = μ

The first convolution power is the original measure.

theorem MeasureTheory.Measure.convolutionPower_succ_absolutelyContinuous {α : Type u_1} [MeasurableSpace α] [AddMonoid α] [MeasurableAdd₂ α] {μ ν : Measure α} [SFinite μ] [ν.IsAddLeftInvariant] (h : μ.AbsolutelyContinuous ν) (n : ℕ) : (μ.convolutionPower (n + 1)).AbsolutelyContinuous ν

Every positive convolution power of an absolutely continuous measure is absolutely continuous with respect to the same left-translation-invariant measure.

theorem MeasureTheory.Measure.convolutionPower_add {α : Type u_1} [MeasurableSpace α] [AddMonoid α] [MeasurableAdd₂ α] (μ : Measure α) [SFinite μ] (m n : ℕ) : μ.convolutionPower (m + n) = (μ.convolutionPower m).conv (μ.convolutionPower n)

Convolution powers turn addition of exponents into convolution.

theorem MeasureTheory.Measure.convolutionPower_succ' {α : Type u_1} [MeasurableSpace α] [AddMonoid α] [MeasurableAdd₂ α] (μ : Measure α) [SFinite μ] (n : ℕ) : μ.convolutionPower (n + 1) = μ.conv (μ.convolutionPower n)

Convolution powers also satisfy the recursion μ^{∗(n + 1)} = μ ∗ μ^{∗n}.

instance MeasureTheory.Measure.isProbabilityMeasure_convolutionPower {α : Type u_1} [MeasurableSpace α] [AddMonoid α] (μ : Measure α) [IsProbabilityMeasure μ] (n : ℕ) : IsProbabilityMeasure (μ.convolutionPower n)

Every convolution power of a probability measure is a probability measure.

theorem MeasureTheory.Measure.measurable_convolutionPower {α : Type u_1} [MeasurableSpace α] [AddMonoid α] [MeasurableAdd₂ α] (n : ℕ) : Measurable fun (μ : ProbabilityMeasure α) => (↑μ).convolutionPower n

On probability measures, each fixed convolution power depends measurably on the measure.

theorem MeasureTheory.Measure.convolutionPower_dirac {α : Type u_1} [MeasurableSpace α] [AddMonoid α] [MeasurableAdd₂ α] (x : α) (n : ℕ) : (dirac x).convolutionPower n = dirac (n • x)

Convolution powers of a point mass add its atom repeatedly.

@[simp]

theorem MeasureTheory.Measure.convolutionPower_dirac_zero {α : Type u_1} [MeasurableSpace α] [AddMonoid α] [MeasurableAdd₂ α] (n : ℕ) : (dirac 0).convolutionPower n = dirac 0

Every convolution power of the point mass at zero is again concentrated at zero.

theorem MeasureTheory.Measure.map_convolutionPower {α : Type u_1} [MeasurableSpace α] [AddMonoid α] [MeasurableAdd₂ α] {β : Type u_2} [MeasurableSpace β] [AddMonoid β] [MeasurableAdd₂ β] (μ : Measure α) [SFinite μ] (f : α →+ β) (hf : Measurable ⇑f) (n : ℕ) : map (⇑f) (μ.convolutionPower n) = (map (⇑f) μ).convolutionPower n

A measurable additive homomorphism transports convolution powers to convolution powers of the pushforward measure.

theorem MeasureTheory.Measure.lintegral_convolutionPower_succ {α : Type u_1} [MeasurableSpace α] [AddMonoid α] [MeasurableAdd₂ α] (μ : Measure α) [SFinite μ] (n : ℕ) (f : α → ENNReal) (hf : Measurable f) : ∫⁻ (z : α), f z ∂μ.convolutionPower (n + 1) = ∫⁻ (x : α), ∫⁻ (y : α), f (x + y) ∂μ ∂μ.convolutionPower n

Integration against a successor convolution power is iterated integration against the preceding power and one further copy of the measure.

theorem MeasureTheory.Measure.conv_sum {α : Type u_1} [MeasurableSpace α] [AddMonoid α] [MeasurableAdd₂ α] {ι : Type u_2} [Countable ι] (μ : Measure α) (ν : ι → Measure α) [∀ (i : ι), SFinite (ν i)] : μ.conv (sum ν) = sum fun (i : ι) => μ.conv (ν i)

Convolution on the left distributes over countable sums of s-finite measures.

theorem MeasureTheory.Measure.conv_Iic_le {M : Type u_2} [MeasurableSpace M] [AddCommMonoid M] [PartialOrder M] [CanonicallyOrderedAdd M] [MeasurableAdd₂ M] [TopologicalSpace M] [OrderClosedTopology M] [OpensMeasurableSpace M] (μ ν : Measure M) (t : M) : (μ.conv ν) (Set.Iic t) ≤ μ (Set.Iic t) * ν (Set.Iic t)

In a canonically ordered additive monoid, the convolution of two measures gives Iic t at most the product of their masses of Iic t, since x + y ≤ t forces x ≤ t and y ≤ t.

theorem MeasureTheory.Measure.bind_conv_bind {E : Type u_2} [AddMonoid E] [MeasurableSpace E] [MeasurableAdd₂ E] {K : ℕ → Measure E} [∀ (n : ℕ), SFinite (K n)] (hK : ∀ (m n : ℕ), K (m + n) = (K m).conv (K n)) (ρ σ : Measure ℕ) : (ρ.bind K).conv (σ.bind K) = (ρ.conv σ).bind K

Mixing a family of measures indexed by ℕ that turns addition into convolution commutes with convolution: (ρ.bind K) ∗ (σ.bind K) = (ρ ∗ σ).bind K when K (m + n) = K m ∗ K n.

@[simp]

theorem MeasureTheory.Measure.charFun_convolutionPower {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] (μ : Measure E) [IsFiniteMeasure μ] (n : ℕ) (t : E) : charFun (μ.convolutionPower n) t = charFun μ t ^ n

The characteristic function of the n-th convolution power of a finite measure is the n-th power of its characteristic function.