English
The inner product of Fourier coefficients equals the inner product of the functions themselves.
Русский
Внутреннее произведение коэффициентов Фурье равно внутреннему произведению функций.
LaTeX
$$$$ \\langle mFourierCoeff(f,i), mFourierCoeff(g,i) \\rangle = \\langle f,g \\rangle.$$$$
Lean4
/-- **Parseval's identity** for inner products: for `L²` functions `f, g` on `UnitAddTorus d`, the
inner product of the Fourier coefficients of `f` and `g` is the inner product of `f` and `g`. -/
theorem hasSum_prod_mFourierCoeff (f g : L²(UnitAddTorus d)) :
HasSum (fun i ↦ conj (mFourierCoeff f i) * (mFourierCoeff g i)) (∫ t, conj (f t) * g t) :=
by
simp_rw [mul_comm (conj _)]
refine HasSum.congr_fun (mFourierBasis.hasSum_inner_mul_inner f g) (fun n ↦ ?_)
simp only [← mFourierBasis_repr, HilbertBasis.repr_apply_apply, inner_conj_symm, mul_comm (inner ℂ f _)]
