fourierCoeff — Mathlib

English

As above, for each p and n, the a.e. equality between fourierLp p n and fourier n holds, i.e., the Lp representative matches the monomial a.e.

Русский

Как выше,a для каждого p и n справедливо равенство ae между fourierLp p n и fourier n: представитель Lp совпадает почти повсюду с мономиалой.

LaTeX

$$fourierLp p n =ᵐ[haarAddCircle] fourier n$$

Lean4

/-- The `n`-th Fourier coefficient of a function `AddCircle T → E`, for `E` a complete normed
`ℂ`-vector space, defined as the integral over `AddCircle T` of `fourier (-n) t • f t`. -/
def fourierCoeff (f : AddCircle T → E) (n : ℤ) : E :=
  ∫ t : AddCircle T, fourier (-n) t • f t ∂haarAddCircle

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