Theorems · Theorem · abstract harmonic analysis

MeasureTheory.convolution_lsmul_swap

∀ {𝕜 : Type u𝕜} {G : Type uG} {F : Type uF} [inst : NormedAddCommGroup F] {x : G} [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_4 : NormedSpace ℝ F]
  [inst_5 : AddCommGroup G] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] [MeasurableNeg G] [MeasurableAdd G] {f : G → 𝕜}
  {g : G → F}, MeasureTheory.convolution f g (ContinuousLinearMap.lsmul 𝕜 𝕜) μ x = ∫ (t : G), f (x - t) • g t ∂μ

The symmetric definition of convolution where the bilinear operator is scalar multiplication.

Defined in

Mathlib.Analysis.Convolution

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNontriviallyNormedFieldNormedSpaceMeasurableSpaceNormedSpaceAddCommGroupMeasureTheory.Measure.IsAddLeftInvariantMeasureTheory.Measure.IsNegInvariantMeasurableNegMeasurableAdd