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.

Fourier coefficients of a lattice periodisation

Statement

Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $f \in S (R^{n})$ , let $Λ$ be a full-rank lattice with dual $Λ^{*}$ and fundamental parallelotope $F$ , and let $P : = P_{Λ} f$ be the periodisation of Schwartz periodisation over a lattice is smooth with locally uniformly summable derivatives. Then for every $λ^{*} \in Λ^{*}$ , $\int_{F} P (x) e^{- 2 π i λ^{*} \cdot x} d x = \hat{f} (λ^{*}), so the normalised coefficient is \frac{1}{covol (Λ)} \int_{F} P (x) e^{- 2 π i λ^{*} \cdot x} d x = \frac{\hat{f} (λ^{*})}{covol (Λ)},$ with $\hat{f}$ the $L^{1}$ Fourier transform of Fourier transform on complex L1 classes.

Facts & Assumptions

Given: Countable Choice, $f \in S (R^{n})$ (Schwartz space and its seminorms), a full-rank lattice $Λ = A Z^{n}$ with dual $Λ^{*} = A^{- T} Z^{n}$ and fundamental parallelotope $F = A ((0, 1]^{n})$ , the periodisation $P (x) = \sum_{λ \in Λ} f (x + λ)$ of Schwartz periodisation over a lattice is smooth with locally uniformly summable derivatives, and $λ^{*} \in Λ^{*}$ (Full-rank lattices, covolume, and the dual lattice, Fundamental parallelotopes of a lattice tile Euclidean space with covolume volume).

[F1]

The translates $F + λ$ , $λ \in Λ$ , are pairwise disjoint and cover $R^{n}$ (Fundamental parallelotopes of a lattice tile Euclidean space with covolume volume); $P$ converges absolutely at every point with locally uniformly summable derivative series (Schwartz periodisation over a lattice is smooth with locally uniformly summable derivatives).

[F2]

Tonelli and Fubini apply on the $σ$ -finite product of the counting measure on $Λ$ and Lebesgue measure on $F$ (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product, Fubini's theorem for L^1 functions on a sigma-finite product).

[F3]

Translation substitution: $\int_{F + λ} g (y) d y = \int_{F} g (x + λ) d x$ for integrable $g$ , by the translation invariance of Lebesgue measure (Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation) and the change-of-variables formula for $L^{1}$ functions (A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions).

[F4]

$f \in L^{1} (R^{n}; C)$ , so $\hat{f} (λ^{*}) = \int_{R^{n}} f (y) e^{- 2 π i λ^{*} \cdot y} d y$ is defined (Schwartz derivatives are integrable, Fourier transform on complex L1 classes).

[F5]

For $λ^{*} \in Λ^{*}$ and $λ \in Λ$ one has $λ^{*} \cdot λ \in Z$ , hence $e^{- 2 π i λ^{*} \cdot (y - λ)} = e^{- 2 π i λ^{*} \cdot y} e^{2 π i λ^{*} \cdot λ} = e^{- 2 π i λ^{*} \cdot y}$ (Full-rank lattices, covolume, and the dual lattice, $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential, $\ker (\exp) = 2 π i Z$ , and $\exp z = \exp w$ exactly when $z - w \in 2 π i Z$ ).

Proof

technique · direct

1.1F1F2F3F4givenalgebra

Because $F + λ$ tile $R^{n}$ [F1], translation substitution [F3] and Tonelli [F2] give $\sum_{λ \in Λ} \int_{F} ∣ f (x + λ) ∣ d x = \int_{R^{n}} ∣ f (y) ∣ d y < \infty$ by [F4]. Since $∣ e^{- 2 π i λ^{*} \cdot x} ∣ = 1$ , the same absolute majorant controls $f (x + λ) e^{- 2 π i λ^{*} \cdot x}$ ; hence the absolutely convergent series defining $P$ may be integrated term by term over the finite-measure set $F$ , and $\int_{F} P (x) e^{- 2 π i λ^{*} \cdot x} d x = \sum_{λ} \int_{F} f (x + λ) e^{- 2 π i λ^{*} \cdot x} d x$ by [F2].

2.1step 1.1F1F3F4F5given

In the $λ$ -th term substitute $y = x + λ$ [F3]: $\int_{F} f (x + λ) e^{- 2 π i λ^{*} \cdot x} d x = \int_{F + λ} f (y) e^{- 2 π i λ^{*} \cdot (y - λ)} d y = \int_{F + λ} f (y) e^{- 2 π i λ^{*} \cdot y} d y$ by [F5]. Summing over $λ$ , the disjointness and covering property [F1] identify the sum of the cell integrals with the integral over $R^{n}$ (countable additivity for the absolutely convergent sums of step 1.1), so $\int_{F} P (x) e^{- 2 π i λ^{*} \cdot x} d x = \int_{R^{n}} f (y) e^{- 2 π i λ^{*} \cdot y} d y = \hat{f} (λ^{*})$ by [F4].

3.1step 2.1given∎

Dividing by $covol (Λ) = ∣ \det A ∣ > 0$ gives the displayed normalised coefficient. Countable Choice is inherited from the Euclidean integration and change-of-variables suppliers above; the lattice indexing is the explicit bijection $λ = A k \leftrightarrow k \in Z^{n}$ .

Depends on

Used by

Poisson summation for a full-rank lattice Theorem

Dependency tree · two levels

92 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

Lior Silberman, Fourier series and the Poisson summation formula (Math 604/613 notes, UBC) (standard reference, not scraped)
Michael E. Taylor, Fourier Analysis, Distributions, and Constant-Coefficient Linear PDE (author PDF) (standard reference, not scraped)