InformationTheory.Shannon.NormalizedSinc

Imports 5

Whittaker-Shannon sampling (partial, Cover-Thomas) #

Companion to ShannonHartley/Main.lean. Mathlib does not ship the Whittaker-Shannon sampling theorem f(t) = Σ_{n ∈ ℤ} f(n/(2W)) · sincN(2W·t - n) for f ∈ L²(ℝ) bandlimited to [-W, W].

This file publishes the subset of the Whittaker-Shannon machinery available in current Mathlib:

sincN x := Real.sinc (π · x) — normalized sinc whose zeros are at the integers.
sincN_int_eq_zero — the integer-zero identity sincN (n : ℝ) = 0 for n ≠ 0.
whittaker_shannon_sample_collapse — sincN((2W)·(n₀/(2W)) − n) = δ_{n,n₀}.

Main statements #

sincN_le_one, neg_one_le_sincN — pointwise bounds.
continuous_sincN, measurable_sincN — regularity.
sincN_int_eq_zero, sincN_int_eq_kronecker — zeros at nonzero integers.
whittaker_shannon_sample_collapse — sample-point collapse (Kronecker delta form).

Implementation notes #

L²-orthogonality of {sincN(·-n)}_{n ∈ ℤ} requires the Fourier transform of the rectangular pulse and Plancherel; Poisson summation requires Schwartz-class results. Neither is available in Mathlib, so both are out of scope here.

§B — Normalized sinc and bridge to Mathlib's `Real.sinc`. #

noncomputable def

InformationTheory.Shannon.NormalizedSinc.sincN

source

(x : ℝ) :

ℝ

Normalized sinc, sin(π · x) / (π · x) (with value 1 at 0).

This is the information-theoretic convention whose zeros land at the non-zero integers (vs Mathlib's Real.sinc whose zeros are at non-zero multiples of π). The Whittaker-Shannon series formula f(t) = Σ_n f(n/(2W)) · sincN(2W·t - n) uses this convention.

Equations

InformationTheory.Shannon.NormalizedSinc.sincN x = Real.sinc (Real.pi * x)

Instances For

Used by

theorem

InformationTheory.Shannon.NormalizedSinc.sincN_zero

source

@[simp]

sincN 0 = 1

Used by

theorem

InformationTheory.Shannon.NormalizedSinc.sincN_le_one

source

(x : ℝ) :

sincN x ≤ 1

Used by

theorem

InformationTheory.Shannon.NormalizedSinc.neg_one_le_sincN

source

(x : ℝ) :

-1 ≤ sincN x

Used by

theorem

InformationTheory.Shannon.NormalizedSinc.sincN_neg

source

(x : ℝ) :

sincN (-x) = sincN x

Used by

theorem

InformationTheory.Shannon.NormalizedSinc.continuous_sincN

source

Continuous sincN

Used by

theorem

InformationTheory.Shannon.NormalizedSinc.measurable_sincN

source

Measurable sincN

Used by

theorem

InformationTheory.Shannon.NormalizedSinc.sincN_of_ne_zero

source

(x : ℝ) (hx : x ≠ 0) :

sincN x = Real.sin (Real.pi * x) / (Real.pi * x)

Used by

§C — Integer-zero identity (sincN Kronecker delta). #

theorem

InformationTheory.Shannon.NormalizedSinc.sincN_int_eq_zero

source

(n : ℤ) (hn : n ≠ 0) :

sincN ↑n = 0

The normalized sinc vanishes at all non-zero integers.

This is the algebraic reason the Whittaker-Shannon series collapses to a single term at a sample point: sincN(n - n₀) = δ_{n,n₀}.

Used by

theorem

InformationTheory.Shannon.NormalizedSinc.sincN_int_eq_kronecker

source

(n : ℤ) :

sincN ↑n = if n = 0 then 1 else 0

Kronecker-delta form of sincN at integers.

Used by

§D — Sample-point collapse identity. #

theorem

InformationTheory.Shannon.NormalizedSinc.whittaker_shannon_sample_collapse

source

(W : ℝ) (hW : 0 < W) (n n₀ : ℤ) :

sincN (2 * W * (↑n₀ / (2 * W)) - ↑n) = if n = n₀ then 1 else 0

The sample-point collapse identity: at t = n₀ / (2W), the Whittaker-Shannon series term sincN(2W·t - n) evaluates to δ_{n,n₀} (1 if n = n₀, 0 otherwise).

This is the rigorous form of "only the n = n₀ term survives" — the information-theoretic content driving the Whittaker-Shannon series collapse at sample points.

Used by