Theorems · Theorem · abstract harmonic analysis

MeasureTheory.Measure.map_conv_continuousLinearMap

∀ {E : Type u_2} {F : Type u_3} [inst : AddCommMonoid E] [inst_1 : AddCommMonoid F] [inst_2 : Module ℝ E]
  [inst_3 : Module ℝ F] [inst_4 : TopologicalSpace E] [inst_5 : TopologicalSpace F] {mE : MeasurableSpace E}
  [MeasurableAdd₂ E] {mF : MeasurableSpace F} [MeasurableAdd₂ F] [OpensMeasurableSpace E] [BorelSpace F]
  {μ ν : MeasureTheory.Measure E} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] (L : E →L[ℝ] F),
  MeasureTheory.Measure.map (⇑L) (μ.conv ν) = (MeasureTheory.Measure.map (⇑L) μ).conv (MeasureTheory.Measure.map (⇑L) ν)

Defined in

Mathlib.MeasureTheory.Group.Convolution

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommMonoidAddCommMonoidModuleModuleTopologicalSpaceTopologicalSpaceMeasurableAdd₂MeasurableAdd₂OpensMeasurableSpaceBorelSpaceMeasureTheory.SFiniteMeasureTheory.SFinite