English
The family of Fourier monomials forms an orthonormal set in L2(AddCircle(T), ℂ) with respect to the normalized Haar measure when 0 < T.
Русский
Мономиалы Фурье образуют ортонормированный набор в L2(AddCircle(T), ℂ) по нормализованной мере Хаара при 0 < T.
LaTeX
$$Orthonormal ℂ (fourierLp 2)$$
Lean4
/-- The monomials `fourier n` are an orthonormal set with respect to normalised Haar measure. -/
theorem orthonormal_fourier : Orthonormal ℂ (@fourierLp T _ 2 _) :=
by
rw [orthonormal_iff_ite]
intro i j
rw [ContinuousMap.inner_toLp (@haarAddCircle T hT) (fourier i) (fourier j)]
simp_rw [← fourier_neg, ← fourier_add]
split_ifs with h
· simp_rw [h, add_neg_cancel]
have : ⇑(@fourier T 0) = (fun _ => 1 : AddCircle T → ℂ) := by ext1; exact fourier_zero
rw [this, integral_const, measureReal_univ_eq_one, Complex.real_smul, Complex.ofReal_one, mul_one]
have hij : j + -i ≠ 0 := by exact sub_ne_zero.mpr (Ne.symm h)
convert integral_eq_zero_of_add_right_eq_neg (μ := haarAddCircle) (fourier_add_half_inv_index hij hT.elim)
