LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Band-limited samples are the Fourier coefficients of the rescaled spectrum

Statement

Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $h > 0$ and let $f \in L^{2} (R; C)$ have Plancherel transform $\hat{f} : = F_{2} f$ (Plancherel theorem) vanishing almost everywhere off the band $[- 1 / (2 h), 1 / (2 h)]$ . Then $\hat{f} \in L^{1}$ , so $f$ has a continuous representative, again written $f$ , with $f (x) = \int_{R} \hat{f} (ξ) e^{2 π i x ξ} d ξ$ for every $x$ . Choose a measurable representative of $\hat{f}$ , set $G_{h} (θ) : = h^{- 1 / 2} \hat{f} (- θ / h)$ on the half-open interval $[- 1 / 2, 1 / 2)$ , and extend $G_{h}$ one-periodically to $R$ . Its almost-everywhere class is independent of the chosen representative and defines a function class on the circle $T = R / Z$ (The one-dimensional torus and its normalized Haar integral). Then $G_{h} \in L^{2} (T; C)$ , and for every $k \in Z$ its $k$ -th Fourier coefficient (Fourier coefficients and trigonometric polynomials on the torus) is $\hat{G_{h}} (k) = h^{1 / 2} f (h k) .$ Consequently $(h^{1 / 2} f (h k))_{k \in Z} \in ℓ^{2} (Z)$ and $\sum_{k \in Z} ∣ f (h k) ∣^{2} = h^{- 1} ∥ f ∥_{L^{2} (R)}^{2} .$ The reflection $θ \mapsto - θ$ in the definition of $G_{h}$ is inserted only so that the library's negative-sign coefficient convention matches the samples $f (h k)$ rather than $f (- h k)$ .

Facts & Assumptions

[F1]

Plancherel: Fourier transformation on Schwartz space extends uniquely to a surjective complex-linear isometry $F_{2} : L^{2} (R; C) \to L^{2} (R; C)$ preserving inner products (Plancherel theorem).

[F2]

Inversion: $F_{2}^{2} f = R f$ with $R f (x) = f (- x)$ , and $F_{2}^{- 1} = R F_{2}$ (L2 Fourier inversion).

[F3]

Agreement: if $g \in L^{1} \cap L^{2}$ , its bounded continuous integral transform $\hat{g} (ξ) = \int g (x) e^{- 2 π i x ξ} d x$ represents $F_{2} g$ almost everywhere (Agreement of the integral and L2 transforms).

[F4]

The integral transform maps $L^{1} (R; C)$ complex-linearly into the bounded uniformly continuous functions, with $\sup_{ξ} ∣ \hat{g} (ξ) ∣ \leq ∥ g ∥_{1}$ (The L1 transform is bounded and uniformly continuous).

[F5]

Finite-measure inclusion: on a measure space of finite measure, $L^{r} \subseteq L^{p}$ for $1 \leq p < r < \infty$ with $∥ g ∥_{p} \leq μ (X)^{1 / p - 1 / r} ∥ g ∥_{r}$ (Finite-measure $L^{r}$ includes into $L^{p}$ for $p < r$ ).

[F6]

$C^{1}$ change of variables for $L^{1}$ functions on open subsets of $R$ (A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions).

[F7]

Riesz–Fischer: the Fourier coefficient map $Φ : L^{2} (T; C) \to ℓ^{2} (Z; C)$ is a surjective linear isometry, so $\sum_{k} ∣ \hat{G} (k) ∣^{2} = ∥ G ∥_{L^{2} (T)}^{2}$ (Riesz–Fischer: the Fourier coefficient map is onto the space of square-summable families).

[F8]

The torus integral is integration of the representative on $[0, 1)$ against $λ_{1}$ , and $\hat{G} (k) = \int_{T} G e_{- k} d m_{T}$ with $e_{- k} (θ) = e^{- 2 π i k θ}$ (The one-dimensional torus and its normalized Haar integral, Fourier coefficients and trigonometric polynomials on the torus).

[F9]

The band $B = [- 1 / (2 h), 1 / (2 h)]$ has measure $1 / h$ , and its endpoints are null (A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included).

Given: Countable Choice, $h > 0$ , a class $f \in L^{2} (R; C)$ with $\hat{f} = F_{2} f$ vanishing almost everywhere off $B : = [- 1 / (2 h), 1 / (2 h)]$ , and the $L^{2}$ classes of The space $L^{p} (μ)$ as the quotient by null functions.

Proof

1.1F5F9givenalgebra

The class $\hat{f}$ is represented by $\hat{f} 1_{B}$ , which lies in $L^{2} (B)$ with the same norm, and $B$ has finite Lebesgue measure $1 / h$ by [F9]. Applying [F5] on $B$ with $p = 1$ , $r = 2$ gives $\hat{f} \in L^{1} (R; C)$ with $∥ \hat{f} ∥_{1} \leq (1 / h)^{1 / 2} ∥ \hat{f} ∥_{2}$ .

2.1F1F2F3F4step 1.1algebra

Define $H (x) : = \int_{R} \hat{f} (ξ) e^{2 π i x ξ} d ξ$ for $x \in R$ . Since $ξ \mapsto \hat{f} (ξ) e^{2 π i x ξ}$ has modulus $∣ \hat{f} ∣ \in L^{1}$ by step 1.1, the integral converges absolutely, and $x \mapsto H (x) = \hat{g} (- x)$ with $g : = \hat{f} \in L^{1} \cap L^{2}$ ; hence $H$ is bounded and continuous by [F4] and reflection. By [F3], $g$ 's integral transform represents $F_{2} g = F_{2} \hat{f} = R f$ almost everywhere by [F2], so $H$ represents $R (R f) = f$ almost everywhere. Replacing the class $f$ by its continuous representative $H$ gives $f (x) = \int_{R} \hat{f} (ξ) e^{2 π i x ξ} d ξ$ for every $x$ , and this replacement changes no $L^{2}$ class.

3.1F1F6F8F9step 2.1algebra

Represent $G_{h}$ on the fundamental interval $[0, 1)$ by $G_{h} (θ) = h^{- 1 / 2} \hat{f} (- \tilde{θ} / h)$ , where $\tilde{θ}$ is the unique representative of $θ + Z$ in $[- 1 / 2, 1 / 2)$ . Substituting $ξ = - θ / h$ on $(0, 1 / 2)$ and $ξ = (1 - θ) / h$ on $(1 / 2, 1)$ , and integrating $∣ G_{h} ∣^{2}$ with [F6], the factor $h^{- 1}$ from $∣ G_{h} ∣^{2}$ cancels the Jacobian $h$ , giving $\int_{T} ∣ G_{h} ∣^{2} d m_{T} = \int_{- 1 / (2 h)}^{1 / (2 h)} ∣ \hat{f} (ξ) ∣^{2} d ξ = ∥ \hat{f} ∥_{2}^{2} = ∥ f ∥_{2}^{2}$ , so $G_{h} \in L^{2} (T; C)$ . The endpoints are null, and the same substitutions show that changing the spectrum on a null set changes $G_{h}$ only on a null set. The same two substitutions applied to $G_{h} e_{- k}$ , using $e^{- 2 π i k (1 - h ξ)} = e^{2 π i k h ξ}$ on the right piece, supply the Jacobian $h$ to the prefactor $h^{- 1 / 2}$ and give $\hat{G_{h}} (k) = h^{1 / 2} \int_{- 1 / (2 h)}^{1 / (2 h)} \hat{f} (ξ) e^{2 π i k h ξ} d ξ = h^{1 / 2} f (h k)$ , the last equality being step 2.1 evaluated at $x = h k$ .

4.1F7step 3.1algebra∎

By step 3.1 and [F7], $\sum_{k \in Z} ∣ h^{1 / 2} f (h k) ∣^{2} = ∥ Φ (G_{h}) ∥^{2} = ∥ G_{h} ∥^{2} = ∥ f ∥_{2}^{2}$ . Since the left side is $h \sum_{k} ∣ f (h k) ∣^{2}$ , dividing by $h$ gives $\sum_{k} ∣ f (h k) ∣^{2} = h^{- 1} ∥ f ∥_{L^{2} (R)}^{2}$ , and in particular $(h^{1 / 2} f (h k))_{k \in Z} \in ℓ^{2} (Z)$ .

Depends on

Used by

Shannon reconstruction of a sinc function Example
Shannon sampling for band-limited L² functions Theorem

Dependency tree · two levels

108 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)