Theorems · Theorem · harmonic analysis

VectorFourier.fourierPowSMulRight_eq_comp

∀ {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]
  (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E} {v : V} {n : ℕ},
  VectorFourier.fourierPowSMulRight L f v n =
    (-(2 * ↑Real.pi * Complex.I)) ^ n •
      ((ContinuousMultilinearMap.smulRightL ℝ (fun x => W) E)
          ((ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x => L v))
        (f v)

Decomposing fourierPowSMulRight L f v n as a composition of continuous bilinear and multilinear maps, to deduce easily its continuity and differentiability properties.

Defined in

Mathlib.Analysis.Fourier.FourierTransformDeriv

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace