`BookProof.ChapterPaleyWienerSampling.BandLimited.hasSum_sq_samples` (hf : BandLimited T f) : HasSum (fun n : ℤ => ‖f ((n : ℝ) / T)‖ ^ 2) (T * ∫ ξ : ℝ, ‖𝓕 f ξ‖ ^ 2)

Initializing...

`BookProof.ChapterPaleyWienerSampling.BandLimited.hasSum_sq_samples` (hf : BandLimited T f) : HasSum (fun n : ℤ => ‖f ((n : ℝ) / T)‖ ^ 2) (T * ∫ ξ : ℝ, ‖𝓕 f ξ‖ ^ 2) · Prove2Me