English
The elements of the basis fourierBasis correspond to the FourierLp functions; in particular, the basis elements coincide with the Fourier monomials on the circle, viewed as L^2-functions.
Русский
Элементы базы fourierBasis соответствуют функциям fourierLp; в частности, базисные элементы совпадают с мононимиалами Фурье на круге, рассматриваемыми как функции в L^2.
LaTeX
$$$$ \\text{coe}_{\\text{fourierBasis}} = \\mathrm{fourierLp}_{2} $$$$
Lean4
/-- The elements of the Hilbert basis `fourierBasis` are the functions `fourierLp 2`, i.e. the
monomials `fourier n` on the circle considered as elements of `L²`. -/
@[simp]
theorem coe_fourierBasis : ⇑(@fourierBasis T hT) = @fourierLp T hT 2 _ :=
HilbertBasis.coe_mk _ _
