English
The Fourier basis is defined as a Z-indexed Hilbert basis for the L^2 space on AddCircle, given by the Fourier monomials. It provides a complete orthonormal set for L^2.
Русский
База Фурье — это Z-инденсированная гильбертовская база пространства L^2 на AddCircle, заданная мономиями Фурье; она образует полную ортонормированную систему.
LaTeX
$$$$ \text{fourierBasis} : \mathrm{HilbertBasis}_{\\mathbb{Z},\\mathbb{C}}(L^{2}(\mathrm{haarAddCircle})) $$$$
Lean4
/-- We define `fourierBasis` to be a `ℤ`-indexed Hilbert basis for `Lp ℂ 2 haarAddCircle`,
which by definition is an isometric isomorphism from `Lp ℂ 2 haarAddCircle` to `ℓ²(ℤ, ℂ)`. -/
def fourierBasis : HilbertBasis ℤ ℂ (Lp ℂ 2 <| @haarAddCircle T hT) :=
HilbertBasis.mk orthonormal_fourier (span_fourierLp_closure_eq_top (by simp)).ge
