InformationTheory.Shannon.WhittakerShannon

Imports 8

Whittaker–Shannon sampling theorem (Fourier-series route, Cover–Thomas) #

This file proves the Whittaker–Shannon (cardinal series) sampling theorem via the L² Fourier series on the circle route, reusing the normalized sinc scaffolding of NormalizedSinc.lean.

The honest core (unconditional) is whittaker_shannon_hasSum: for an L² spectrum F : Lp ℂ 2 (haarAddCircle (T := 1)), the reconstructed signal wsSignal F is recovered from its integer samples by the cardinal series wsSignal F t = ∑' n, wsSignal F n · sincN (t - n) (as a HasSum).

Main statements #

wsExp — the evaluation kernel ξ ↦ e^{-2πiξt} as an L² element of AddCircle 1.
wsSignal — the band-limited signal reconstructed from an L² spectrum F.
inner_wsExp_fourierLp — the monomial pairing collapses to a normalized sinc.
fourierCoeff_eq_wsSignal — a Fourier coefficient equals a sample value.
whittaker_shannon_hasSum — the cardinal series, per-t HasSum form (unconditional).
whittaker_shannon_bandlimited — real-line band-limited textbook wrapper (stretch).

instance

InformationTheory.Shannon.WhittakerShannon.instFactLtRealOfNat_informationTheory

source

Fact (0 < 1)

Fact (0 < 1) so AddCircle 1 carries haarAddCircle.

Used by

noncomputable def

InformationTheory.Shannon.WhittakerShannon.wsExpFun

source

(t : ℝ) :

ℝ → ℂ

The evaluation kernel as a real-line function s ↦ e^{-2πist}.

Equations

InformationTheory.Shannon.WhittakerShannon.wsExpFun t s = Complex.exp (↑(-(2 * Real.pi * t * s)) * Complex.I)

Instances For

Used by

noncomputable def

InformationTheory.Shannon.WhittakerShannon.wsExp

source

(t : ℝ) :

↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)

The evaluation kernel ξ ↦ e^{-2πiξt} as an L² element of the unit circle.

Equations

InformationTheory.Shannon.WhittakerShannon.wsExp t = MeasureTheory.MemLp.toLp (AddCircle.liftIoc 1 (-(1 / 2)) (InformationTheory.Shannon.WhittakerShannon.wsExpFun t)) ⋯

Instances For

Used by

noncomputable def

InformationTheory.Shannon.WhittakerShannon.wsSignal

source

(F : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) (t : ℝ) :

ℂ

The reconstructed band-limited signal, ⟪wsExp t, F⟫.

Equations

InformationTheory.Shannon.WhittakerShannon.wsSignal F t = inner ℂ (InformationTheory.Shannon.WhittakerShannon.wsExp t) F

Instances For

Used by

theorem

InformationTheory.Shannon.WhittakerShannon.integral_exp_boxcar_eq_sincN

source

(s : ℝ) :

∫ (a : ℝ) in -(1 / 2)..1 / 2, Complex.exp (↑(2 * Real.pi * s * a) * Complex.I) = ↑(NormalizedSinc.sincN s)

The boxcar integral over the unit interval equals the normalized sinc.

Used by

theorem

InformationTheory.Shannon.WhittakerShannon.inner_wsExp_fourierLp

source

(t : ℝ) (n : ℤ) :

inner ℂ (wsExp t) (fourierLp 2 n) = ↑(NormalizedSinc.sincN (t + ↑n))

Step 4 bridge: the monomial pairing is the normalized sinc.

Used by

theorem

InformationTheory.Shannon.WhittakerShannon.fourierCoeff_eq_wsSignal

source

(F : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) (n : ℤ) :

fourierCoeff (↑↑F) n = wsSignal F (-↑n)

Step 3 bridge: the Fourier coefficient is the sample value.

Used by

theorem

InformationTheory.Shannon.WhittakerShannon.whittaker_shannon_hasSum

source

(F : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) (t : ℝ) :

HasSum (fun (n : ℤ) => wsSignal F ↑n • ↑(NormalizedSinc.sincN (t - ↑n))) (wsSignal F t)

Whittaker–Shannon, per-t HasSum on an L² spectrum (unconditional core).

@audit:ok. Unconditional: signature is (F : Lp ℂ 2 haarAddCircle) (t : ℝ) with no load-bearing hypothesis and the conclusion is not assumed among the inputs; #print axioms = [propext, Classical.choice, Quot.sound] (sorryAx-free). Genuinely captures the sampling theorem (wsSignal F t = ⟪wsExp t, F⟫ is the inverse-Fourier reconstruction, F ranges over the band-limited spectra).

Used by

theorem

InformationTheory.Shannon.WhittakerShannon.whittaker_shannon_bandlimited

source

(f : ℝ → ℂ) (hcont : Continuous f) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hFf : MeasureTheory.Integrable (FourierTransform.fourier f) MeasureTheory.volume) (hband : ∀ ξ ∉ Set.Icc (-(1 / 2)) (1 / 2), FourierTransform.fourier f ξ = 0) (t : ℝ) :

HasSum (fun (n : ℤ) => f ↑n • ↑(NormalizedSinc.sincN (t - ↑n))) (f t)

Whittaker–Shannon, real-line band-limited textbook wrapper (statement (i)).

Reduces to whittaker_shannon_hasSum by taking F to be 𝓕 f restricted to the fundamental interval as a circle-L² element; Fourier inversion (Continuous.fourierInv_fourier_eq) plus the band-limited support hypothesis give wsSignal F w = f w for every real w.

Used by