ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Shannon reconstruction of a sinc function

Example

Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )) and let $sinc$ be the normalised sinc of The normalised sinc function. Then $\overset{}{sinc} = 1_{[- 1 / 2, 1 / 2]}$ as $L^{2}$ Fourier transforms, so $sinc$ is band-limited with $h = 1$ and band $[- 1 / 2, 1 / 2]$ ; its samples are $sinc (k) = 1$ for $k = 0$ and $sinc (k) = 0$ for every nonzero integer $k$ ; and the Shannon series of Shannon sampling for band-limited $L^{2}$ functions for this $f$ is $\sum_{k \in Z} sinc (k) sinc (x - k) = sinc (x)$ , a single nonzero term at $k = 0$ reproducing the function at every $x$ . Since $\sum_{k} ∣ sinc (k) ∣ = 1 < \infty$ , the locally uniform clause of the theorem applies as well. The example checks the signs, the band endpoints $\pm 1 / 2$ and the $h^{1 / 2}$ normalisation of the pair.

Facts & Assumptions

Given: Countable Choice, the normalised sinc of The normalised sinc function and the interval indicator $1 = 1_{[- 1 / 2, 1 / 2]}$ .

[F1]

Interval indicator transform, computed from the primitive: for real $t$ , $\int_{- 1 / 2}^{1 / 2} e^{- 2 π i t ξ} d ξ = sinc (t)$ , because $u (ξ) = e^{- 2 π i t ξ} / (- 2 π i t)$ has $u^{'} = e^{- 2 π i t ξ}$ (The complex exponential is entire and its complex derivative is itself, The chain rule for complex derivatives) so the complex FTC gives $(\sin (π t) / (π t))$ for $t \neq 0$ by oddness of sine (Complex integration by parts on intervals and decaying lines, Parity and the Pythagorean identity for sine and cosine), while at $t = 0$ the integral is $1 = sinc (0)$ (The normalised sinc function); $1 \in L^{1} \cap L^{2}$ .

[F2]

On $L^{1} \cap L^{2}$ the integral transform represents the $L^{2}$ transform almost everywhere (Agreement of the integral and L2 transforms); $F_{2}^{2} = R$ with $R g (x) = g (- x)$ (L2 Fourier inversion).

[F3]

Shannon sampling theorem: for $f \in L^{2}$ band-limited to $[- 1 / (2 h), 1 / (2 h)]$ with continuous representative $f$ , $f = \sum_{k} f (h k) sinc (\cdot / h - k)$ in $L^{2}$ , and the identity is pointwise everywhere when $\sum_{k} ∣ f (h k) ∣ < \infty$ (Shannon sampling for band-limited $L^{2}$ functions).

[F4]

Band-limit normalisation check of Band-limited samples are the Fourier coefficients of the rescaled spectrum: for $h = 1$ the rescaled circular function is $G_{1} (θ) = \hat{f} (- θ)$ and its coefficients satisfy $\hat{G_{1}} (k) = 1^{1 / 2} f (k) = f (k)$ .

Verification

1.1F1F2givenalgebra

By [F1] the $L^{1}$ transform of $1$ is $sinc$ , so the $L^{2}$ transform of $1$ is represented by $sinc$ [F2]. Since $sinc$ is bounded by the two bounds of The normalised sinc function, it lies in $L^{2}$ , and $F_{2} (sinc) = F_{2} (F_{2} 1) = R 1 = 1$ , the last equality because $1$ is even and $1 \circ (- 1) = 1$ .

2.1step 1.1F3F4givenalgebra∎

Thus $sinc$ is band-limited with $h = 1$ and band $[- 1 / 2, 1 / 2]$ , and its samples are $sinc (0) = 1$ and $sinc (k) = 0$ for nonzero integers $k$ (The normalised sinc function). Its Shannon series therefore has the single nonzero term at $k = 0$ : $\sum_{k} sinc (k) sinc (x - k) = sinc (x)$ for every $x$ , and $\sum_{k} ∣ sinc (k) ∣ = 1 < \infty$ , so both clauses of [F3] hold and the reconstruction is pointwise everywhere. The normalisation check [F4] also matches: here $\hat{f} = 1$ , so $G_{1} (θ) = 1 (- θ) = 1$ on the fundamental interval and $\hat{G_{1}} (k) = 1$ for $k = 0$ and $0$ otherwise, which equals $1^{1 / 2} sinc (k)$ ; the Fourier pair is the interval indicator and $sinc$ , with $F_{2} sinc = 1_{[- 1 / 2, 1 / 2]}$ . Values at the band endpoints do not affect these $L^{2}$ classes.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

55 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Richard S. Laugesen, Harmonic Analysis Lecture Notes (arXiv:0903.3845) (standard reference, not scraped)
Lior Silberman, Fourier series and the Poisson summation formula (Math 604/613 notes, UBC) (standard reference, not scraped)