theorem FourierOrthonormalBasis.fourier_hilbertBasis {T : ℝ} [hT : Fact (0 < T)] : ∃ (b : HilbertBasis ℤ ℂ ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)), ⇑b = fourierLp 2