The multiplicative and additive convolution of measures

In this file we define and prove properties about the convolutions of two measures.

Main definitions

• MeasureTheory.Measure.mconv: The multiplicative convolution of two measures: the map of * under the product measure.
• MeasureTheory.Measure.conv: The additive convolution of two measures: the map of + under the product measure.

noncomputable def MeasureTheory.Measure.mconv {M : Type u_1} [Monoid M] [MeasurableSpace M] (μ ν : Measure M) : Measure M

Multiplicative convolution of measures.

noncomputable def MeasureTheory.Measure.conv {M : Type u_1} [AddMonoid M] [MeasurableSpace M] (μ ν : Measure M) : Measure M

Additive convolution of measures.

def MeasureTheory.«term_∗ₘ_» : Lean.TrailingParserDescr

Scoped notation for the multiplicative convolution of measures.

def MeasureTheory.«term_∗_» : Lean.TrailingParserDescr

Scoped notation for the additive convolution of measures.

theorem MeasureTheory.Measure.lintegral_mconv_eq_lintegral_prod {M : Type u_1} [Monoid M] [MeasurableSpace M] [MeasurableMul₂ M] {μ ν : Measure M} {f : M → ENNReal} (hf : Measurable f) : ∫⁻ (z : M), f z ∂μ.mconv ν = ∫⁻ (z : M × M), f (z.1 * z.2) ∂μ.prod ν

theorem MeasureTheory.Measure.lintegral_conv_eq_lintegral_sum {M : Type u_1} [AddMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] {μ ν : Measure M} {f : M → ENNReal} (hf : Measurable f) : ∫⁻ (z : M), f z ∂μ.conv ν = ∫⁻ (z : M × M), f (z.1 + z.2) ∂μ.prod ν

theorem MeasureTheory.Measure.lintegral_mconv {M : Type u_1} [Monoid M] [MeasurableSpace M] [MeasurableMul₂ M] {μ ν : Measure M} [SFinite ν] {f : M → ENNReal} (hf : Measurable f) : ∫⁻ (z : M), f z ∂μ.mconv ν = ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ν ∂μ

theorem MeasureTheory.Measure.lintegral_conv {M : Type u_1} [AddMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] {μ ν : Measure M} [SFinite ν] {f : M → ENNReal} (hf : Measurable f) : ∫⁻ (z : M), f z ∂μ.conv ν = ∫⁻ (x : M), ∫⁻ (y : M), f (x + y) ∂ν ∂μ

theorem MeasureTheory.Measure.dirac_mconv {M : Type u_1} [Monoid M] [MeasurableSpace M] [MeasurableMul₂ M] (x : M) (μ : Measure M) [SFinite μ] : (dirac x).mconv μ = map (fun (y : M) => x * y) μ

theorem MeasureTheory.Measure.dirac_conv {M : Type u_1} [AddMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] (x : M) (μ : Measure M) [SFinite μ] : (dirac x).conv μ = map (fun (y : M) => x + y) μ

theorem MeasureTheory.Measure.mconv_dirac {M : Type u_1} [Monoid M] [MeasurableSpace M] [MeasurableMul₂ M] (μ : Measure M) [SFinite μ] (x : M) : μ.mconv (dirac x) = map (fun (y : M) => y * x) μ

theorem MeasureTheory.Measure.conv_dirac {M : Type u_1} [AddMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] (μ : Measure M) [SFinite μ] (x : M) : μ.conv (dirac x) = map (fun (y : M) => y + x) μ

@[simp]

theorem MeasureTheory.Measure.dirac_mconv_dirac {M : Type u_1} [Monoid M] [MeasurableSpace M] [MeasurableMul₂ M] (x y : M) : (dirac x).mconv (dirac y) = dirac (x * y)

@[simp]

theorem MeasureTheory.Measure.dirac_conv_dirac {M : Type u_1} [AddMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] (x y : M) : (dirac x).conv (dirac y) = dirac (x + y)

@[simp]

theorem MeasureTheory.Measure.dirac_one_mconv {M : Type u_1} [Monoid M] [MeasurableSpace M] [MeasurableMul₂ M] (μ : Measure M) [SFinite μ] : (dirac 1).mconv μ = μ

Convolution of the dirac measure at 1 with a measure μ returns μ.

@[simp]

theorem MeasureTheory.Measure.dirac_zero_conv {M : Type u_1} [AddMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] (μ : Measure M) [SFinite μ] : (dirac 0).conv μ = μ

Convolution of the dirac measure at 0 with a measure μ returns μ.

@[simp]

theorem MeasureTheory.Measure.mconv_dirac_one {M : Type u_1} [Monoid M] [MeasurableSpace M] [MeasurableMul₂ M] (μ : Measure M) [SFinite μ] : μ.mconv (dirac 1) = μ

Convolution of a measure μ with the dirac measure at 1 returns μ.

@[simp]

theorem MeasureTheory.Measure.conv_dirac_zero {M : Type u_1} [AddMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] (μ : Measure M) [SFinite μ] : μ.conv (dirac 0) = μ

Convolution of a measure μ with the dirac measure at 0 returns μ.

@[simp]

theorem MeasureTheory.Measure.zero_mconv {M : Type u_1} [Monoid M] [MeasurableSpace M] (μ : Measure M) : mconv 0 μ = 0

Convolution of the zero measure with a measure μ returns the zero measure.

@[simp]

theorem MeasureTheory.Measure.zero_conv {M : Type u_1} [AddMonoid M] [MeasurableSpace M] (μ : Measure M) : conv 0 μ = 0

Convolution of the zero measure with a measure μ returns the zero measure.

@[simp]

theorem MeasureTheory.Measure.mconv_zero {M : Type u_1} [Monoid M] [MeasurableSpace M] (μ : Measure M) : μ.mconv 0 = 0

Convolution of a measure μ with the zero measure returns the zero measure.

@[simp]

theorem MeasureTheory.Measure.conv_zero {M : Type u_1} [AddMonoid M] [MeasurableSpace M] (μ : Measure M) : μ.conv 0 = 0

Convolution of a measure μ with the zero measure returns the zero measure.

theorem MeasureTheory.Measure.mconv_smul_left {M : Type u_1} [Monoid M] [MeasurableSpace M] (μ ν : Measure M) [SFinite ν] (s : ENNReal) : (s • μ).mconv ν = s • μ.mconv ν

theorem MeasureTheory.Measure.conv_smul_left {M : Type u_1} [AddMonoid M] [MeasurableSpace M] (μ ν : Measure M) [SFinite ν] (s : ENNReal) : (s • μ).conv ν = s • μ.conv ν

theorem MeasureTheory.Measure.mconv_add {M : Type u_1} [Monoid M] [MeasurableSpace M] [MeasurableMul₂ M] (μ ν ρ : Measure M) [SFinite μ] [SFinite ν] [SFinite ρ] : μ.mconv (ν + ρ) = μ.mconv ν + μ.mconv ρ

theorem MeasureTheory.Measure.conv_add {M : Type u_1} [AddMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] (μ ν ρ : Measure M) [SFinite μ] [SFinite ν] [SFinite ρ] : μ.conv (ν + ρ) = μ.conv ν + μ.conv ρ

theorem MeasureTheory.Measure.add_mconv {M : Type u_1} [Monoid M] [MeasurableSpace M] [MeasurableMul₂ M] (μ ν ρ : Measure M) [SFinite μ] [SFinite ν] [SFinite ρ] : (μ + ν).mconv ρ = μ.mconv ρ + ν.mconv ρ

theorem MeasureTheory.Measure.add_conv {M : Type u_1} [AddMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] (μ ν ρ : Measure M) [SFinite μ] [SFinite ν] [SFinite ρ] : (μ + ν).conv ρ = μ.conv ρ + ν.conv ρ

theorem MeasureTheory.Measure.mconv_comm {M : Type u_2} [CommMonoid M] [MeasurableSpace M] [MeasurableMul₂ M] (μ ν : Measure M) [SFinite μ] [SFinite ν] : μ.mconv ν = ν.mconv μ

To get commutativity, we need the underlying multiplication to be commutative.

theorem MeasureTheory.Measure.conv_comm {M : Type u_2} [AddCommMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] (μ ν : Measure M) [SFinite μ] [SFinite ν] : μ.conv ν = ν.conv μ

To get commutativity, we need the underlying addition to be commutative.

instance MeasureTheory.Measure.sfinite_mconv_of_sfinite {M : Type u_1} [Monoid M] [MeasurableSpace M] (μ ν : Measure M) [SFinite μ] [SFinite ν] : SFinite (μ.mconv ν)

The convolution of s-finite measures is s-finite.

instance MeasureTheory.Measure.sfinite_conv_of_sfinite {M : Type u_1} [AddMonoid M] [MeasurableSpace M] (μ ν : Measure M) [SFinite μ] [SFinite ν] : SFinite (μ.conv ν)

The convolution of s-finite measures is s-finite.

instance MeasureTheory.Measure.finite_of_finite_mconv {M : Type u_1} [Monoid M] [MeasurableSpace M] (μ ν : Measure M) [IsFiniteMeasure μ] [IsFiniteMeasure ν] : IsFiniteMeasure (μ.mconv ν)

instance MeasureTheory.Measure.finite_of_finite_conv {M : Type u_1} [AddMonoid M] [MeasurableSpace M] (μ ν : Measure M) [IsFiniteMeasure μ] [IsFiniteMeasure ν] : IsFiniteMeasure (μ.conv ν)

theorem MeasureTheory.Measure.mconv_assoc {M : Type u_1} [Monoid M] [MeasurableSpace M] [MeasurableMul₂ M] (μ ν ρ : Measure M) [SFinite ν] [SFinite ρ] : (μ.mconv ν).mconv ρ = μ.mconv (ν.mconv ρ)

Convolution is associative.

theorem MeasureTheory.Measure.conv_assoc {M : Type u_1} [AddMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] (μ ν ρ : Measure M) [SFinite ν] [SFinite ρ] : (μ.conv ν).conv ρ = μ.conv (ν.conv ρ)

Convolution is associative.

instance MeasureTheory.Measure.probabilitymeasure_of_probabilitymeasures_mconv {M : Type u_1} [Monoid M] [MeasurableSpace M] (μ ν : Measure M) [MeasurableMul₂ M] [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] : IsProbabilityMeasure (μ.mconv ν)

instance MeasureTheory.Measure.probabilitymeasure_of_probabilitymeasures_conv {M : Type u_1} [AddMonoid M] [MeasurableSpace M] (μ ν : Measure M) [MeasurableAdd₂ M] [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] : IsProbabilityMeasure (μ.conv ν)

theorem MeasureTheory.Measure.mconv_absolutelyContinuous {M : Type u_1} [Monoid M] [MeasurableSpace M] [MeasurableMul₂ M] {μ ν ρ : Measure M} [ρ.IsMulLeftInvariant] [SFinite ν] (hν : ν.AbsolutelyContinuous ρ) : (μ.mconv ν).AbsolutelyContinuous ρ

theorem MeasureTheory.Measure.conv_absolutelyContinuous {M : Type u_1} [AddMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] {μ ν ρ : Measure M} [ρ.IsAddLeftInvariant] [SFinite ν] (hν : ν.AbsolutelyContinuous ρ) : (μ.conv ν).AbsolutelyContinuous ρ

theorem MeasureTheory.Measure.map_mconv_monoidHom {M : Type u_2} {M' : Type u_3} {mM : MeasurableSpace M} [Monoid M] [MeasurableMul₂ M] {mM' : MeasurableSpace M'} [Monoid M'] [MeasurableMul₂ M'] {μ ν : Measure M} [SFinite μ] [SFinite ν] (L : M →* M') (hL : Measurable ⇑L) : map (⇑L) (μ.mconv ν) = (map (⇑L) μ).mconv (map (⇑L) ν)

theorem MeasureTheory.Measure.map_conv_addMonoidHom {M : Type u_2} {M' : Type u_3} {mM : MeasurableSpace M} [AddMonoid M] [MeasurableAdd₂ M] {mM' : MeasurableSpace M'} [AddMonoid M'] [MeasurableAdd₂ M'] {μ ν : Measure M} [SFinite μ] [SFinite ν] (L : M →+ M') (hL : Measurable ⇑L) : map (⇑L) (μ.conv ν) = (map (⇑L) μ).conv (map (⇑L) ν)

theorem MeasureTheory.Measure.map_conv_continuousLinearMap {E : Type u_2} {F : Type u_3} [AddCommMonoid E] [AddCommMonoid F] [Module ℝ E] [Module ℝ F] [TopologicalSpace E] [TopologicalSpace F] {mE : MeasurableSpace E} [MeasurableAdd₂ E] {mF : MeasurableSpace F} [MeasurableAdd₂ F] [OpensMeasurableSpace E] [BorelSpace F] {μ ν : Measure E} [SFinite μ] [SFinite ν] (L : E →L[ℝ] F) : map (⇑L) (μ.conv ν) = (map (⇑L) μ).conv (map (⇑L) ν)