Nyquist–Shannon sampling theorem

DefinitionUnnormalised cardinal sine#✓fully proved

The function \(\operatorname{sinc} \colon \mathbb{R} \to \mathbb{C}\) is defined by \(\operatorname{sinc}(x) = \frac{\sin x}{x}\) for \(x \neq 0\) and \(\operatorname{sinc}(0) = 1\), the value that removes the singularity at \(0\). Its values are real.

The Whittaker–Shannon interpolation formula evaluates \(\operatorname{sinc}\) at \(0\) at the integer sample points, so the value at \(0\) is part of the definition.

noncomputable def sinc (x : ℝ) : ℂ :=
  if x = 0 then 1 else ((Real.sin x / x : ℝ) : ℂ)

Used by 1

Used byNyquist–Shannon sampling theorem (Whittaker–Shannon interpolation formula)

DefinitionFourier support in the Nyquist band#✓fully proved

A Schwartz function \(f \colon \mathbb{R} \to \mathbb{C}\) has Fourier support in the Nyquist band when its Fourier transform \(\hat f(\xi) = \int_{\mathbb{R}} f(x)\, e^{-2\pi i x \xi}\, dx\) vanishes at every real \(\xi\) outside the closed interval \([-\frac12, \frac12]\).

def FourierSupportedInNyquist (f : 𝓢(ℝ, ℂ)) : Prop :=
  ∀ ξ : ℝ, ξ ∉ Icc (-(1 / 2 : ℝ)) (1 / 2 : ℝ) → 𝓕 f ξ = 0

Used by 1

Used byNyquist–Shannon sampling theorem (Whittaker–Shannon interpolation formula)

TheoremNyquist–Shannon sampling theorem (Whittaker–Shannon interpolation formula)#●ready to prove

Let \(\operatorname{sinc}(x) = \frac{\sin x}{x}\) for real \(x \neq 0\) and \(\operatorname{sinc}(0) = 1\), and let \(f \colon \mathbb{R} \to \mathbb{C}\) be a Schwartz function whose Fourier transform \(\hat f(\xi) = \int_{\mathbb{R}} f(x)\, e^{-2\pi i x \xi}\, dx\) vanishes at every real \(\xi\) outside \([-\frac12, \frac12]\). Then for every real \(t\) the series \(\sum_{n \in \mathbb{Z}} f(n) \operatorname{sinc}(\pi(n - t))\) is summable over \(\mathbb{Z}\) (unconditionally convergent) and

\[ f(t) = \sum_{n \in \mathbb{Z}} f(n) \operatorname{sinc}(\pi(n - t)). \]

public theorem_wanted nyquist_shannon_sampling (f : 𝓢(ℝ, ℂ)) (hf : FourierSupportedInNyquist f) :
    ∀ t : ℝ,
      Summable (fun n : ℤ ↦ f (n : ℝ) * sinc (Real.pi * ((n : ℝ) - t))) ∧
        f t =
          ∑' n : ℤ, f (n : ℝ) * sinc (Real.pi * ((n : ℝ) - t))

Sources

• 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. Problem nyquist_shannon_sampling of the lean-eval benchmark.

Uses 2

Statement usesFourier support in the Nyquist band · Unnormalised cardinal sine

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.