Theorems · Theorem · harmonic analysis

SchwartzMap.convolution_apply

∀ {E : Type u_3} {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [inst : NormedAddCommGroup E]
  [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E]
  [inst_5 : NormedAddCommGroup F₁] [inst_6 : NormedSpace ℂ F₁] [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace ℂ F₂] [inst_9 : NormedAddCommGroup F₃] [inst_10 : NormedSpace ℂ F₃] [CompleteSpace F₃]
  [CompleteSpace F₁] [CompleteSpace F₂] (B : F₁ →L[ℂ] F₂ →L[ℂ] F₃) (f : SchwartzMap E F₁) (g : SchwartzMap E F₂)
  (x : E), (((SchwartzMap.convolution B) f) g) x = MeasureTheory.convolution (⇑f) (⇑g) B MeasureTheory.volume x

The convolution on Schwartz functions is equal to the convolution on functions.

Defined in

Mathlib.Analysis.Fourier.Convolution

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceFiniteDimensionalMeasurableSpaceBorelSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceCompleteSpaceCompleteSpaceCompleteSpace