Theorems · Definition · harmonic analysis

UnitAddTorus.mFourierCoeff

{d : Type u_1} →
  [Fintype d] → {E : Type u_2} → [inst : NormedAddCommGroup E] → [NormedSpace ℂ E] → (UnitAddTorus d → E) → (d → ℤ) → E

The n-th Fourier coefficient of a function UnitAddTorus d → E, for E a complete normed ℂ-vector space, defined as the integral over UnitAddTorus d of mFourier (-n) t • f t.

Defined in

Mathlib.Analysis.Fourier.AddCircleMulti

Cited by

8 results in Mathlib

Foundations

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

Assumes

FintypeNormedAddCommGroupNormedSpace