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.

The Dirac comb of a full-rank lattice transforms to the dual comb

Statement

Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $Λ$ be a full-rank lattice with covolume $c$ and dual $Λ^{*}$ . The $Λ$ -Dirac comb ${comb}_{Λ} : = \sum_{λ \in Λ} δ_{λ}$ , defined by $⟨ {comb}_{Λ}, φ ⟩ = \sum_{λ} φ (λ)$ , is a tempered distribution, and $F {comb}_{Λ} = c^{- 1} {comb}_{Λ^{*}} in S^{'} (R^{n}),$ that is, $⟨ F {comb}_{Λ}, φ ⟩ = c^{- 1} \sum_{λ^{*} \in Λ^{*}} φ (λ^{*})$ for every $φ \in S (R^{n})$ . For $Λ = Z^{n}$ ( $c = 1$ , $Λ^{*} = Z^{n}$ ) this is Fourier-invariance of the unit comb, the published Dirac comb is fourier invariant; the scaled case here ( $Λ = h Z^{n}$ , $c = h^{n}$ ) is what the sampling lemma below consumes.

Facts & Assumptions

Given: Countable Choice, the full-rank lattice $Λ = A Z^{n}$ with covolume $c$ and dual $Λ^{*} = A^{- T} Z^{n}$ (Full-rank lattices, covolume, and the dual lattice), the Dirac distributions $δ_{λ}$ (Dirac delta and its derivatives), and the unit comb conventions of Dirac comb.

[F1]

For every integer $L \geq 0$ and every $x \in R^{n}$ , $∣ φ (x) ∣ \leq A_{n, L} (1 + ∣ x ∣)^{- L} \max_{∣ α ∣ \leq L} p_{α, 0} (φ)$ . Indeed $1 + ∣ x ∣ \leq 1 + \sum_{j} ∣ x_{j} ∣$ , whose $L$ th power is a finite sum of monomials $∣ x^{α} ∣$ with $∣ α ∣ \leq L$ and positive coefficients by The multinomial coefficient equals $n! / \prod_{i < m} k_{i}!$ , and $(x_{0} + \dots + x_{m - 1})^{n} = \sum ι ⁣ (\binom{n}{k}) \prod_{i < m} x_{i}^{k_{i}}$ in $R$ ; multiplying by $∣ φ (x) ∣$ bounds each monomial by its seminorm (Schwartz space and its seminorms). At integer points this is the unit-comb estimate of Dirac comb.

[F2]

Transporting shells by $λ = A k$ : $∣ λ ∣ \leq r$ implies $∣ k ∣ \leq K r$ for a constant $K$ , and conversely $m \leq ∣ λ ∣ < m + 1$ implies $m / K^{'} \leq ∣ k ∣ < K^{'} (m + 1)$ for constants, so the shell has at most $C (1 + m)^{n}$ lattice points; likewise for $Λ^{*} = A^{- T} Z^{n}$ (Every Euclidean linear map has a unique matrix and satisfies $∥ L h ∥_{2} \leq K ∥ h ∥_{2}$ for some $K \geq 0$ , Full-rank lattices, covolume, and the dual lattice).

[F3]

$\sum_{m \geq 1} m^{n - L} < \infty$ for real $L > n + 1$ ; a finite-seminorm bound characterises tempered distributions (The p-series for a real exponent p converges exactly when p is greater than one, Finite seminorm bound characterizes tempered distributions).

[F4]

The Fourier transform of a tempered distribution is defined by $⟨ F u, φ ⟩ = ⟨ u, F φ ⟩$ (Fourier transform of a tempered distribution), and on Schwartz functions $F^{2} = R$ with $R φ (x) = φ (- x)$ (Fourier transform is a topological automorphism of Schwartz space).

[F5]

Poisson summation for a full-rank lattice: for $ψ \in S (R^{n})$ , $\sum_{λ \in Λ} ψ (λ) = c^{- 1} \sum_{λ^{*} \in Λ^{*}} \hat{ψ} (λ^{*})$ (Poisson summation for a full-rank lattice).

Proof

technique · direct

1.1F1F2F3givenalgebra

Fix an integer $L > n + 1$ . For $φ \in S$ , the bound of [F1] and the shell count of [F2] give $\sum_{λ \in Λ} ∣ φ (λ) ∣ \leq A_{n, L} \sum_{m \geq 0} C (1 + m)^{n} (1 + m)^{- L} \max_{∣ α ∣ \leq L} p_{α, 0} (φ)$ , which is finite by [F3]; hence the series defining ${comb}_{Λ}$ converges absolutely and satisfies a single finite-seminorm estimate, so ${comb}_{Λ}$ is a tempered distribution by [F3]. On a compactly supported test only finitely many $δ_{λ}$ remain, matching the locally finite sum of Dirac delta and its derivatives, so the definition is the intended one.

2.1step 1.1F4F5givenalgebra

For $φ \in S$ , the definition of the distributional transform [F4] and the definition of the comb give $⟨ F {comb}_{Λ}, φ ⟩ = ⟨ {comb}_{Λ}, F φ ⟩ = \sum_{λ \in Λ} \hat{φ} (λ)$ . Applying the lattice Poisson formula [F5] to the Schwartz function $ψ : = \hat{φ}$ , and using $F^{2} = R$ on Schwartz functions [F4], $\sum_{λ} \hat{φ} (λ) = c^{- 1} \sum_{λ^{*}} \hat{\hat{φ}} (λ^{*}) = c^{- 1} \sum_{λ^{*}} φ (- λ^{*})$ . The map $λ^{*} \mapsto - λ^{*}$ is a bijection of the group $Λ^{*}$ , so the last sum equals $c^{- 1} \sum_{λ^{*}} φ (λ^{*}) = ⟨ c^{- 1} {comb}_{Λ^{*}}, φ ⟩$ .

3.1step 2.1F5given∎

Equality of the two tempered distributions on every Schwartz test proves $F {comb}_{Λ} = c^{- 1} {comb}_{Λ^{*}}$ ; at $Λ = Z^{n}$ , where $c = 1$ and $Λ^{*} = Z^{n}$ , this specialises to the published unit-comb theorem Dirac comb is fourier invariant, which is hereby a cross-check rather than a supplier. Countable Choice is inherited from the Poisson theorem and the distributional Fourier interface.

Depends on

Used by

Sampling at a lattice produces periodisation of the spectrum over the dual lattice Lemma

Dependency tree · two levels

94 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)
Noam Elkies, Theta functions and weighted theta functions of Euclidean lattices (author PDF) (standard reference, not scraped)