English
The second coe relation between mFourierBasis and mFourierLp(2) holds under index change.
Русский
Вторая связь по коэффициентам между mFourierBasis и mFourierLp(2) сохраняется при смене индекса.
LaTeX
$$$$ \\text{coe}_{\\text{mFourierBasis}} = mFourierLp(2). $$$$
Lean4
/-- Under the isometric isomorphism `mFourierBasis` from `L²(UnitAddTorus d)` to `ℓ²(ℤᵈ, ℂ)`,
the `i`-th coefficient is `mFourierCoeff f i`. -/
theorem mFourierBasis_repr (f : L²(UnitAddTorus d)) (i : d → ℤ) : mFourierBasis.repr f i = mFourierCoeff f i :=
by
trans ∫ t, conj (mFourierLp 2 i t) * f t
· rw [mFourierBasis.repr_apply_apply f i, MeasureTheory.L2.inner_def, coe_mFourierBasis]
simp only [RCLike.inner_apply, mul_comm]
· apply integral_congr_ae
filter_upwards [coeFn_mFourierLp 2 i] with _ ht
rw [ht, ← mFourier_neg, smul_eq_mul]
