Theorems · Definition · harmonic analysis

VectorFourier.fourierSMulRight

{E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℂ E] →
      {V : Type u_2} →
        {W : Type u_3} →
          [inst_2 : NormedAddCommGroup V] →
            [inst_3 : NormedSpace ℝ V] →
              [inst_4 : NormedAddCommGroup W] →
                [inst_5 : NormedSpace ℝ W] → (V →L[ℝ] W →L[ℝ] ℝ) → (V → E) → V → W →L[ℝ] E

Send a function f : V → E to the function f : V → Hom (W, E) given by v ↦ (w ↦ -2 * π * I * L (v, w) • f v). This is designed so that the Fourier transform of fourierSMulRight L f is the derivative of the Fourier transform of f.

Defined in

Mathlib.Analysis.Fourier.FourierTransformDeriv

Cited by

15 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace