TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 2026-09-22

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 Fourier basis and Parseval's identity on the finite torus

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $n \geq 1$ and let $e_{k} (x) = \exp (2 π i k \cdot x)$ , $k \in Z^{n}$ , be the coordinate characters on $T^{n}$ (The one-dimensional torus and its normalized Haar integral, Fourier coefficients and trigonometric polynomials on the torus). Then:

$(e_{k})_{k \in Z^{n}}$ is an orthonormal family in the complex Hilbert space $L^{2} (T^{n})$ ;
it is an orthonormal basis: its closed linear span is $L^{2} (T^{n})$ ;
consequently the Fourier expansion $f = \sum_{k \in Z^{n}} \hat{f} (k) e_{k}$ and Parseval's identity $∥ f ∥_{2}^{2} = \sum_{k \in Z^{n}} ∣ \hat{f} (k) ∣^{2}, ⟨ f, g ⟩ = \sum_{k \in Z^{n}} \hat{f} (k) \overline{\hat{g} (k)}$ hold for all $f, g \in L^{2} (T^{n})$ , in the finite-subset-net sense; and
the Fourier coefficient map is a surjective linear isometry of $L^{2} (T^{n})$ onto $ℓ^{2} (Z^{n}, C)$ .

No Hilbert tensor-product identification is used anywhere.

Facts & Assumptions

[A1]

On the product measure $m_{T^{n}}$ Fubini's theorem computes iterated integrals of $L^{1}$ functions, and for a product of functions $h (x) = \prod_{j} h_{j} (x_{j})$ with each $h_{j} \in L^{1} (m_{T})$ the integral is the product $\prod_{j} \int h_{j} d m_{T}$ , by applying Fubini one coordinate at a time; each character has modulus one, so $e_{k} \overline{e_{l}}$ is bounded and hence in $L^{1}$ . In one dimension, the character family is orthonormal (Fubini's theorem for L^1 functions on a sigma-finite product, The one-dimensional torus and its normalized Haar integral, The trigonometric characters are orthonormal in $L^{2}$ of the torus).

[A2]

$T^{n}$ is compact Hausdorff and its coordinate characters separate points (Finite tori are compact Hausdorff spaces separated by characters).

[A3]

The trigonometric polynomials on $T^{n}$ are uniformly dense in $C (T^{n}, C)$ by the unital case of complex Stone–Weierstrass, and the continuous functions are dense in $L^{2} (T^{n})$ ; on the probability space $T^{n}$ one has $∥ g ∥_{2} \leq ∥ g ∥_{\infty}$ (Complex Stone–Weierstrass dichotomy for separating self-adjoint algebras; the unital case is dense, Continuous functions are dense in $L^{p}$ of finite tori and of bounded intervals, Finite-measure $L^{r}$ includes into $L^{p}$ for $p < r$ ).

[A4]

$L^{2} (T^{n})$ is a complex Hilbert space with inner product $\int f \overline{g}$ ( $L^{2}$ with the integral pairing is a Hilbert space), and for a Hilbert space with an orthonormal basis the expansion, Parseval identity and surjectivity of the coefficient isometry hold (Fourier expansion in a Hilbert space, A Hilbert space with a given orthonormal basis is $ℓ^{2}$ of the index set).

[A5]

Orthonormality of a family means $⟨ e_{k}, e_{l} ⟩ = δ_{k l}$ ; completeness means the closed linear span is the whole space (Orthonormal families, complete orthonormal systems and Hilbert bases).

Proof

technique · direct

Given: Countable Choice, $n \geq 1$ , and the coordinate characters $e_{k}$ on $T^{n}$ .

1.1

For $k, l \in Z^{n}$ , Fubini and separation of variables give $⟨ e_{k}, e_{l} ⟩ = \int_{T^{n}} \prod_{j < n} e_{k_{j}} (x_{j}) \overline{e_{l_{j}} (x_{j})} d m_{T^{n}} = \prod_{j < n} \int_{T} e_{k_{j}} \overline{e_{l_{j}}} d m_{T}$ , where each factor is $δ_{k_{j} l_{j}}$ by orthonormality of the one-dimensional characters; the product is $δ_{k l}$ .

A1A5

1.2

The algebra generated by the coordinate characters is unital, self-adjoint and point-separating, so by complex Stone–Weierstrass the trigonometric polynomials on $T^{n}$ are uniformly dense in $C (T^{n}, C)$ ; hence for $f \in L^{2} (T^{n})$ and $ε > 0$ there is a trigonometric polynomial $p$ with $∥ f - p ∥_{2} < 2 ε$ , by first approximating $f$ in $L^{2}$ by a continuous function and then that function uniformly, using $∥ \cdot ∥_{2} \leq ∥ \cdot ∥_{\infty}$ .

A2A3

2.1

Since the linear span of the coordinate characters is exactly the set of trigonometric polynomials, step 1.2 shows that the closed linear span of $(e_{k})$ is all of $L^{2} (T^{n})$ , that is, the family is orthonormal and complete, hence an orthonormal basis.

step 1.1step 1.2A5

3.1

By the general Fourier expansion and coefficient-isometry theorems applied to this basis, every $f$ is the finite-subset-net sum $\sum_{k \in Z^{n}} \hat{f} (k) e_{k}$ , Parseval's norm and pairing identities hold, and the Fourier coefficient map is a surjective linear isometry onto $ℓ^{2} (Z^{n}, C)$ .

step 2.1A4

4.1

Steps 1.1, 2.1 and 3.1 establish orthonormality, basis property, expansion and Parseval with the coefficient isometry, all without invoking any tensor-product identification of $L^{2} (T^{n})$ with a tensor power.

step 1.1step 2.1step 3.1∎

Depends on

Used by

Fourier series on a torus as Peter–Weyl Example

Dependency tree · two levels

111 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

Theo Bühler and Dietmar Salamon, Functional Analysis — §§2.3.6 and 5.3.1, pp.87–88 and 235–237 (standard reference, not scraped)
Gerald Teschl, Topics in Real and Functional Analysis, version November 17, 2017 — §2.5, pp.63–68 (standard reference, not scraped)