Theorems · Theorem · abstract harmonic analysis

MeasureTheory.Measure.map_conv_addMonoidHom

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

Defined in

Mathlib.MeasureTheory.Group.Convolution

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddMonoidMeasurableAdd₂AddMonoidMeasurableAdd₂MeasureTheory.SFiniteMeasureTheory.SFinite