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.

Orthogonality of the lattice characters over a fundamental domain

Statement

Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $A$ , $Λ = A Z^{n}$ and $F$ be as in Fundamental parallelotopes of a lattice tile Euclidean space with covolume volume, and let $λ^{*}, η^{*} \in Λ^{*}$ . Then $\frac{1}{covol (Λ)} \int_{F} e^{2 π i (λ^{*} - η^{*}) \cdot x} d x = {\begin{cases} 1, & λ^{*} = η^{*}, \\ 0, & λ^{*} \neq η^{*} . \end{cases}$

Facts & Assumptions

Given: Countable Choice, an invertible real $n \times n$ matrix $A$ , the lattice $Λ = A Z^{n}$ with dual $Λ^{*} = A^{- T} Z^{n}$ and covolume $covol (Λ) = ∣ \det A ∣$ , the fundamental parallelotope $F = A ((0, 1]^{n})$ , and $λ^{*}, η^{*} \in Λ^{*}$ (Full-rank lattices, covolume, and the dual lattice, Fundamental parallelotopes of a lattice tile Euclidean space with covolume volume).

[F1]

$λ^{*}, η^{*} \in A^{- T} Z^{n}$ , so $μ : = λ^{*} - η^{*} \in A^{- T} Z^{n}$ and $c : = A^{T} μ \in Z^{n}$ ; conversely $c = 0$ forces $μ = 0$ , because $A^{T}$ is invertible (Full-rank lattices, covolume, and the dual lattice, Transpose is linear and involutive, and $(A B)^{T} = B^{T} A^{T}$ , For every square matrix over a commutative ring, $\det (A^{T}) = \det (A)$ , A finite square real matrix is invertible if and only if its determinant is nonzero, Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes).

[F2]

Change of variables: for the $C^{1}$ diffeomorphism $y \mapsto A y$ on the open unit box, $\int_{F^{\circ}} g (x) d x = ∣ \det A ∣ \int_{(0, 1)^{n}} g (A y) d y$ for nonnegative Lebesgue measurable $g$ (A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions); the boundary $F ∖ F^{\circ} = A ((0, 1]^{n} ∖ (0, 1)^{n})$ is the image under $A$ of a finite union of degenerate boxes, hence a null set (A linear map $T$ of $R^{n}$ sends Lebesgue measurable sets to Lebesgue measurable sets, with $λ_{n} (T [E]) = ∣ \det T ∣ λ_{n} (E)$ when $T$ is invertible and $T [E]$ Lebesgue null when it is not, 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), and integrals over a null set vanish (A nonnegative integral over a null set vanishes).

[F3]

The box integral factorises: for $c \in R^{n}$ , $\int_{(0, 1]^{n}} e^{2 π i c \cdot y} d y = \prod_{j = 1}^{n} \int_{0}^{1} e^{2 π i c_{j} t} d t$ (Fubini's theorem for L^1 functions on a sigma-finite product).

[F4]

One-dimensional character integrals: $\int_{0}^{1} e^{2 π i r t} d t = 1$ when $r = 0$ and $0$ when $r$ is a nonzero integer, by the complex primitive $\int_{0}^{1} e^{2 π i r t} d t = (e^{2 π i r} - 1) / (2 π i r)$ (Complex integration by parts on intervals and decaying lines) together with $e^{2 π i r} = 1$ for integral $r$ ( $\ker (\exp) = 2 π i Z$ , and $\exp z = \exp w$ exactly when $z - w \in 2 π i Z$ ); this is the unit-cube case of the orthonormality of the characters (The trigonometric characters are orthonormal in $L^{2}$ of the torus), and $∣ e^{2 π i c \cdot y} ∣ = 1$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

Proof

technique · direct

1.1F1F2F3F4givenalgebra

Put $μ = λ^{*} - η^{*}$ , so that $c = A^{T} μ \in Z^{n}$ and $e^{2 π i μ \cdot x} = e^{2 π i c \cdot (A^{- 1} x)}$ [F1, F4]. The integrand has modulus one on the finite-measure set $F$ . Apply the nonnegative substitution and null-boundary formulas of [F2] separately to the positive and negative parts of its real and imaginary parts; all four integrals are finite, so recombining them gives the complex substitution formula. Together with [F3], this yields $\int_{F} e^{2 π i μ \cdot x} d x = ∣ \det A ∣ \int_{(0, 1]^{n}} e^{2 π i c \cdot y} d y = ∣ \det A ∣ \prod_{j = 1}^{n} \int_{0}^{1} e^{2 π i c_{j} t} d t$ .

1.2F4givenalgebra

Each factor is evaluated by [F4]: for $c_{j} = 0$ the factor is $\int_{0}^{1} 1 d t = 1$ , and for $c_{j} \in Z ∖ {0}$ it is $(e^{2 π i c_{j}} - 1) / (2 π i c_{j}) = 0$ because $e^{2 π i c_{j}} = 1$ . Hence the product equals $1$ when every $c_{j} = 0$ , and $0$ otherwise.

2.1step 1.1step 1.2F1given∎

Since $c = A^{T} μ$ , we have $c = 0$ if and only if $μ = 0$ , by invertibility of $A^{T}$ [F1]. Dividing the identity of step 1.1 by $covol (Λ) = ∣ \det A ∣$ , the product of step 1.2 is exactly the normalised integral, so it equals $1$ when $λ^{*} = η^{*}$ and $0$ when $λ^{*} \neq η^{*}$ . Countable Choice is inherited from the change-of-variables interface used in [F2], exactly as in the volume computation of the tiling lemma.

Depends on

Used by

Poisson summation for a full-rank lattice Theorem
Poisson summation under two-sided polynomial decay Theorem

Dependency tree · two levels

119 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)
Richard S. Laugesen, Harmonic Analysis Lecture Notes (arXiv:0903.3845) (standard reference, not scraped)