Nyquist–Shannon sampling theorem

nyquist_shannon_sampling

Submitter: Kim Morrison.

Notes: Whittaker–Shannon interpolation: a Schwartz function f whose Fourier transform is supported in the Nyquist band [-1/2, 1/2] (mathlib's e^{-2π i x ξ} convention) is reconstructed from its integer samples by the cardinal series f(t) = ∑_{n : ℤ} f(n) · sinc(π(n - t)), with the series summable. Trusted helpers (sinc, FourierSupportedInNyquist) are non-holes; the Summable conjunct records convergence rather than relying on Lean's total tsum. Mathlib has Schwartz space, the Fourier transform, inversion, Plancherel and Poisson summation, but not the sampling theorem. Candidate from §179 of the Knill survey.

Source: C. E. Shannon, *Communication in the presence of noise*, Proc. IRE 37 (1949); H. Nyquist (1928); E. T. Whittaker (1915). Knill, *Some fundamental theorems in mathematics*, §179.

Informal solution: Let g = 𝓕 f, supported in [-1/2, 1/2]. Extend g periodically with period 1 and expand it in a Fourier series on [-1/2, 1/2]; the Fourier coefficients are exactly the samples f(n) (up to sign), by Fourier inversion ∫ g(ξ) e^{2π i n ξ} dξ = f(n) since g is band-limited. Substituting this Fourier series for g into the inversion formula f(t) = ∫ g(ξ) e^{2π i t ξ} dξ and integrating term by term (justified by Schwartz decay, giving the Summable claim) produces f(t) = ∑_{n} f(n) ∫_{[-1/2,1/2]} e^{2π i (t - n) ξ} dξ = ∑_{n} f(n) · sinc(π(n - t)), since the band-limited indicator integrates to a cardinal sine. Equivalently this is Poisson summation applied to the band-limited f. Not in Mathlib.

theorem declaration uses `sorry`nyquist_shannon_sampling (f : 𝓢(ℝ, ℂ)) (hf : LeanEval.Analysis.NyquistShannon.FourierSupportedInNyquist f) :
    ∀ t : ℝ,
      Summable (fun n : ℤ ↦ f (n : ℝ) * sinc (Real.pi * ((n : ℝ) - t))) ∧
        f t =
          ∑' n : ℤ, f (n : ℝ) * sinc (Real.pi * ((n : ℝ) - t)) := byf:𝓢(ℝ, ℂ)hf:FourierSupportedInNyquist f⊢ ∀ (t : ℝ), (Summable fun n => f ↑n * sinc (Real.pi * (↑n - t))) ∧ f t = ∑' (n : ℤ), f ↑n * sinc (Real.pi * (↑n - t))
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on Jun 21, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on Jun 21, 2026