mFourierCoeff — Mathlib

English

The basis elements of mFourierBasis coincide with the functions mFourierLp(2).

Русский

Элементы базиса mFourierBasis совпадают с функциями mFourierLp(2).

LaTeX

$$$$\\text{coe}_{{\\text{mFourierBasis}}} = mFourierLp(2).$$$$

Lean4

/-- 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`. -/
def mFourierCoeff (f : UnitAddTorus d → E) (n : d → ℤ) : E :=
  ∫ t, mFourier (-n) t • f t

Похожие утверждения