Documentation

Mathlib.MeasureTheory.Group.Convolution

The multiplicative and additive convolution of measures #

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

Main definitions #

Additive convolution of measures.

Equations
Instances For

    Multiplicative convolution of measures.

    Equations
    Instances For

      Scoped notation for the multiplicative convolution of measures.

      Equations
      Instances For

        Scoped notation for the additive convolution of measures.

        Equations
        Instances For
          @[simp]

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

          @[simp]

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

          @[simp]

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

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

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

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

          Convolution of SFinite maps is SFinite.

          Equations
          • =