`BookProof.ChapterShannonSampling.integrableOn_spectrum` (F : Lp ℂ 2 (haarAddCircle (T := T))) : IntegrableOn (fun ξ : ℝ => (F : AddCircle T → ℂ) ξ) (Ioc (-(T / 2)) (-(T / 2) + T))

Initializing...

`BookProof.ChapterShannonSampling.integrableOn_spectrum` (F : Lp ℂ 2 (haarAddCircle (T := T))) : IntegrableOn (fun ξ : ℝ => (F : AddCircle T → ℂ) ξ) (Ioc (-(T / 2)) (-(T / 2) + T)) · Prove2Me