Theorems · Theorem · harmonic analysis

VectorFourier.fourierPowSMulRight_apply

∀ {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 : ℕ} {m : Fin n → W},
  (VectorFourier.fourierPowSMulRight L f v n) m = (-(2 * ↑Real.pi * Complex.I)) ^ n • (∏ i, (L v) (m i)) • f v

Defined in

Mathlib.Analysis.Fourier.FourierTransformDeriv

Cited by

7 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace