English
The family mFourierLp(2) forms an orthonormal set in L2 on UnitAddTorus d.
Русский
Семейство mFourierLp(2) образует орто-нормированный набор в L2 на UnitAddTorus d.
LaTeX
$$$$\\text{Orthonormal}_{\\mathbb{C}}\\big( f = mFourierLp(2)\\big).$$$$
Lean4
/-- The monomials `mFourierLp 2 n` are an orthonormal set in `L²`. -/
theorem orthonormal_mFourier : Orthonormal ℂ (mFourierLp (d := d) 2) :=
by
rw [orthonormal_iff_ite]
intro m n
simp only [ContinuousMap.inner_toLp, ← mFourier_neg, ← mFourier_add]
split_ifs with h
·
simpa only [h, add_neg_cancel, mFourier_zero, measureReal_univ_eq_one, one_smul] using
integral_const (α := UnitAddTorus d) (μ := volume) (1 : ℂ)
rw [mFourier, ContinuousMap.coe_mk, MeasureTheory.integral_fintype_prod_volume_eq_prod]
obtain ⟨i, hi⟩ := Function.ne_iff.mp h
apply Finset.prod_eq_zero (Finset.mem_univ i)
simpa only [eq_false_intro hi, if_false, ContinuousMap.inner_toLp, ← fourier_neg, ← fourier_add] using
(orthonormal_iff_ite.mp <| orthonormal_fourier) (m i) (n i)
