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.

Riesz–Fischer: the Fourier coefficient map is onto the space of square-summable families

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). The Fourier coefficient map

$Φ : L^{2} (T; C) \to ℓ^{2} (Z, C), Φ (f) : = (\hat{f} (k))_{k \in Z},$

is a surjective linear isometry preserving inner products: $∥ Φ (f) ∥_{2} = ∥ f ∥_{2}$ and $⟨ Φ (f), Φ (g) ⟩_{ℓ^{2}} = ⟨ f, g ⟩$ for all $f, g$ .

Consequently every square-summable family $a \in ℓ^{2} (Z, C)$ is the sequence of Fourier coefficients of a unique class $f \in L^{2} (T; C)$ , namely the $L^{2}$ limit of the partial sums $\sum_{∣ k ∣ \leq N} a_{k} e_{k}$ . This is a surjectivity statement about the coefficient map, not the completeness theorem for $L^{p}$ .

Facts & Assumptions

[A1]

The characters are an orthonormal basis of the complex Hilbert space $L^{2} (T; C)$ (The trigonometric system is complete in $L^{2}$ of the torus, $L^{2}$ with the integral pairing is a Hilbert space).

[A2]

If $(e_{i})_{i \in I}$ is an orthonormal basis of a Hilbert space $H$ , then $x \mapsto (⟨ x, e_{i} ⟩)_{i \in I}$ is a surjective linear isometry $H \to ℓ^{2} (I, F)$ preserving inner products, and $ℓ^{2} (I, F)$ is complete (A Hilbert space with a given orthonormal basis is $ℓ^{2}$ of the index set).

[A3]

$\hat{f} (k) = ⟨ f, e_{k} ⟩$ , so $Φ$ is the coefficient map of the character basis (Fourier coefficients and trigonometric polynomials on the torus).

[A4]

The elements of $ℓ^{2} (Z, C)$ are the square-summable families, and the expansion of an element $a$ in the coordinate vectors is its defining family, so surjectivity of the coefficient map means exactly that every $a$ occurs as $(\hat{f} (k))$ for some $f$ (Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ ).

[A5]

For a complete orthonormal family, the finite-subset net of Fourier partial sums of any vector converges in norm to that vector (Fourier expansion in a Hilbert space).

Proof

technique · direct

Given: Countable Choice and the Fourier coefficient map $Φ$ .

1.1

By [A1] the characters are an orthonormal basis of $L^{2} (T; C)$ , and by [A3] the map $Φ$ is exactly the coefficient map of that basis.

A1A3

2.1

The general coefficient-isometry theorem for Hilbert spaces with a given orthonormal basis therefore applies to $Φ$ : it is a linear bijection onto $ℓ^{2} (Z, C)$ satisfying $∥ Φ (f) ∥_{2} = ∥ f ∥_{2}$ and $⟨ Φ (f), Φ (g) ⟩_{ℓ^{2}} = ⟨ f, g ⟩$ , and the target space is complete.

step 1.1A2

3.1

In particular $Φ$ is surjective: for every $a \in ℓ^{2} (Z, C)$ there is exactly one $f \in L^{2} (T; C)$ with $\hat{f} (k) = a_{k}$ for all $k$ . For this $f$ , [A5] says that the finite-subset net $\sum_{k \in F} \hat{f} (k) e_{k}$ converges to $f$ . Given a finite $F_{0} \subseteq Z$ , some $N_{0}$ has $F_{0} \subseteq {- N_{0}, \dots, N_{0}}$ ; hence the symmetric finite sets are cofinal, and the symmetric sums $\sum_{∣ k ∣ \leq N} a_{k} e_{k}$ converge to $f$ .

step 2.1A4A5

4.1

Steps 2.1 and 3.1 are the announced surjective isometry and the Riesz–Fischer uniqueness of the class realizing a given square-summable coefficient family.

step 2.1step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

57 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

Gerald Teschl, Topics in Real and Functional Analysis, version November 17, 2017 — §2.5, Theorem 2.17, final assertion (standard reference, not scraped)
Theo Bühler and Dietmar Salamon, Functional Analysis — Exercise 2.64, p.87 (standard reference, not scraped)