`BookProof.ChapterPaleyWienerSampling.BandLimited.hasSum_sinc` (hf : BandLimited T f) (x : ℝ) : HasSum (fun n : ℤ => f ((n : ℝ) / T) * (sinc (T * x

Initializing...

`BookProof.ChapterPaleyWienerSampling.BandLimited.hasSum_sinc` (hf : BandLimited T f) (x : ℝ) : HasSum (fun n : ℤ => f ((n : ℝ) / T) * (sinc (T * x - n) : ℝ)) (f x) · Prove2Me