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.conv {M : Type u_1} [AddMonoid M] [MeasurableSpace M] (μ : MeasureTheory.Measure M) (ν : MeasureTheory.Measure M) : MeasureTheory.Measure M

Additive convolution of measures.

Equations

• MeasureTheory.Measure.conv μ ν = MeasureTheory.Measure.map (fun (x : M × M) => x.1 + x.2) (MeasureTheory.Measure.prod μ ν)

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

Multiplicative convolution of measures.

Equations

• MeasureTheory.Measure.mconv μ ν = MeasureTheory.Measure.map (fun (x : M × M) => x.1 * x.2) (MeasureTheory.Measure.prod μ ν)

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

Scoped notation for the multiplicative convolution of measures.

Equations

• MeasureTheory.«term_∗_» = Lean.ParserDescr.trailingNode `MeasureTheory.term_∗_ 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∗ ") (Lean.ParserDescr.cat `term 81))

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

Scoped notation for the additive convolution of measures.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

theorem MeasureTheory.Measure.mconv_zero {M : Type u_1} [Monoid M] [MeasurableSpace M] (μ : MeasureTheory.Measure M) : MeasureTheory.Measure.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] (μ : MeasureTheory.Measure M) : MeasureTheory.Measure.conv μ 0 = 0

@[simp]

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

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

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

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

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

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

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

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

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

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

Equations

• ⋯ = ⋯

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

Convolution of SFinite maps is SFinite.

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯