Theorems · Theorem · abstract harmonic analysis

MeasureTheory.Measure.map_mconv_monoidHom

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

Defined in

Mathlib.MeasureTheory.Group.Convolution

Cited by

0 results in Mathlib

Foundations

Depth 223 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MonoidMeasurableMul₂MonoidMeasurableMul₂MeasureTheory.SFiniteMeasureTheory.SFinite