English
In the Hilbert basis fourierBasis, the i-th coordinate of a function f is its Fourier coefficient; concretely, the repr map yields the i-th coefficient equal to fourierCoeff f i.
Русский
В базе Фурье четыреirBasis i-й коэффициент функции f равен её коэффициенту Фурье fourierCoeff f i.
LaTeX
$$$$ (\\text{fourierBasis.repr } f)_i = \\widehat{f}(i) $$$$
Lean4
/-- Under the isometric isomorphism `fourierBasis` from `Lp ℂ 2 haarAddCircle` to `ℓ²(ℤ, ℂ)`, the
`i`-th coefficient is `fourierCoeff f i`, i.e., the integral over `AddCircle T` of
`fun t => fourier (-i) t * f t` with respect to the Haar measure of total mass 1. -/
theorem fourierBasis_repr (f : Lp ℂ 2 <| @haarAddCircle T hT) (i : ℤ) : fourierBasis.repr f i = fourierCoeff f i :=
by
trans ∫ t : AddCircle T, conj ((@fourierLp T hT 2 _ i : AddCircle T → ℂ) t) * f t ∂haarAddCircle
· rw [fourierBasis.repr_apply_apply f i, MeasureTheory.L2.inner_def, coe_fourierBasis]
simp only [RCLike.inner_apply']
· apply integral_congr_ae
filter_upwards [coeFn_fourierLp 2 i] with _ ht
rw [ht, ← fourier_neg, smul_eq_mul]
