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.
Multiplicative convolution of measures.
Instances For
Additive convolution of measures.
Instances For
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 80))
Instances For
Scoped notation for the additive convolution of measures.
Equations
- MeasureTheory.«term_∗__1» = Lean.ParserDescr.trailingNode `MeasureTheory.«term_∗__1» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∗ ") (Lean.ParserDescr.cat `term 80))
Instances For
Convolution of the dirac measure at 1 with a measure μ returns μ.
Convolution of the dirac measure at 0 with a measure μ returns μ.
Convolution of a measure μ with the dirac measure at 1 returns μ.
Convolution of a measure μ with the dirac measure at 0 returns μ.
Convolution of the zero measure with a measure μ returns the zero measure.
Convolution of the zero measure with a measure μ returns the zero measure.
Convolution of a measure μ with the zero measure returns the zero measure.
Convolution of a measure μ with the zero measure returns the zero measure.
To get commutativity, we need the underlying multiplication to be commutative.
To get commutativity, we need the underlying addition to be commutative.
The convolution of s-finite measures is s-finite.
The convolution of s-finite measures is s-finite.
Convolution is associative.
Convolution is associative.