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.

Fourier expansion in a Hilbert space

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $(e_{i})_{i \in I}$ be a complete orthonormal family in a real or complex Hilbert space $H$ (Orthonormal families, complete orthonormal systems and Hilbert bases) and let $x \in H$ , with partial sums $P_{F} x = \sum_{i \in F} ⟨ x, e_{i} ⟩ e_{i}$ over finite $F \subseteq I$ . Then:

$x$ is the norm limit of the finite-subset net $(P_{F} x)$ , that is $x = \sum_{i \in I} ⟨ x, e_{i} ⟩ e_{i}$ in the sense of convergence of the net of finite subsums;
the coefficients are unique: if $(a_{i})_{i \in I}$ is a family in $F$ whose finite-subset net $\sum_{i \in F} a_{i} e_{i}$ converges to $x$ , then $a_{i} = ⟨ x, e_{i} ⟩$ for every $i \in I$ ;
the support ${i : ⟨ x, e_{i} ⟩ \neq 0}$ is at most countable, and the expansion does not depend on an ordering: if $(i_{k})_{k \in N}$ is a sequence of pairwise distinct elements of $I$ whose image contains the support, then the sequence of partial sums $\sum_{k < n} ⟨ x, e_{i_{k}} ⟩ e_{i_{k}}$ also converges to $x$ .

Claim 3 is the sense in which the expansion is unconditional: the sum is independent of any ordering, because the finite-subset net converges and any enumeration of a set containing the support by pairwise distinct indices is cofinal in the squared mass.

Facts & Assumptions

[A1]

For a complete orthonormal family, the finite-subset net $(P_{F} x)$ converges to $x$ for every $x$ , since completeness is equivalent to net convergence (Parseval equivalences for an orthonormal family).

[A2]

If $z_{F} \to z$ in $H$ then $⟨ z_{F}, v ⟩ \to ⟨ z, v ⟩$ for every $v \in H$ , because $∣ ⟨ z_{F} - z, v ⟩ ∣ \leq ∥ z_{F} - z ∥ ∥ v ∥$ (Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs).

[A3]

The support of the coefficient family is at most countable (Only countably many coefficients of a square-summable family are nonzero, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[A5]

Parseval gives $∥ x ∥^{2} = \sum_{i \in I} ∣ ⟨ x, e_{i} ⟩ ∣^{2}$ for a complete orthonormal family. Combining this with the finite residual identity and the splitting identity for a nonnegative family yields $∥ x - P_{F} x ∥^{2} = \sum_{i \in I ∖ F} ∣ ⟨ x, e_{i} ⟩ ∣^{2}$ . If $F \subseteq G$ , finite Pythagoras gives $∥ P_{G} x - P_{F} x ∥^{2} = \sum_{i \in G ∖ F} ∣ ⟨ x, e_{i} ⟩ ∣^{2}$ (Parseval equivalences for an orthonormal family, The finite Bessel inequality and best approximation by a finite orthonormal family, Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ , Pythagoras and finite orthogonal sums).

[A6]

If $\sum_{i \in I} ∣ a_{i} ∣^{2} < + \infty$ then for every real $ε > 0$ there is a finite $F \subseteq I$ with $\sum_{i \in I ∖ F} ∣ a_{i} ∣^{2} < ε$ (Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ ).

Proof

technique · direct

Given: Countable Choice, a complete orthonormal family $(e_{i})_{i \in I}$ in $H$ , a vector $x \in H$ , and the coefficients $a_{i} : = ⟨ x, e_{i} ⟩$ .

1.1

By completeness the finite-subset net $(P_{F} x)$ converges to $x$ , which is claim 1.

1.2

For claim 2, let $(b_{i})_{i \in I}$ be a family whose finite-subset net $Q_{F} : = \sum_{i \in F} b_{i} e_{i}$ converges to $x$ . Fix $j \in I$ ; for every finite $F ∋ j$ the orthonormality gives $⟨ Q_{F}, e_{j} ⟩ = b_{j}$ , and $Q_{F} \to x$ implies $⟨ Q_{F}, e_{j} ⟩ \to ⟨ x, e_{j} ⟩$ , so the constant net of values $b_{j}$ converges to $⟨ x, e_{j} ⟩$ , that is $b_{j} = ⟨ x, e_{j} ⟩$ .

1.3

The support of $(a_{i})$ is at most countable by the support lemma.

2.1

For claim 3, let $(i_{k})_{k \in N}$ be a sequence of pairwise distinct elements of $I$ whose image contains the support $S$ of $(a_{i})$ , let $E_{n} : = {i_{k} : k < n}$ and put $s_{n} : = \sum_{k < n} a_{i_{k}} e_{i_{k}} = P_{E_{n}} x$ , so each $E_{n}$ is a finite set of $n$ distinct indices. Given a real $ε > 0$ , [A5] with $F = \emptyset$ gives $\sum_{i \in I} ∣ a_{i} ∣^{2} = ∥ x ∥^{2} < + \infty$ , so [A6] supplies a finite $F_{0} \subseteq I$ with $\sum_{i \in I ∖ F_{0}} ∣ a_{i} ∣^{2} < ε^{2}$ ; since every element of the finite set $F_{0} \cap S$ occurs among the $i_{k}$ , choose $n_{0}$ with $F_{0} \cap S \subseteq E_{n_{0}}$ . For $n \geq n_{0}$ we have $F_{0} \cap S \subseteq E_{n}$ , and $(I ∖ E_{n}) \cap S \subseteq I ∖ F_{0}$ . For any finite $G \subseteq I ∖ E_{n}$ , the terms in $G ∖ S$ vanish, while $G \cap S$ is a finite subset of $I ∖ F_{0}$ . Thus its squared-coefficient sum is at most the full tail outside $F_{0}$ ; taking the supremum over such $G$ gives $\sum_{i \in I ∖ E_{n}} ∣ a_{i} ∣^{2} \leq \sum_{i \in I ∖ F_{0}} ∣ a_{i} ∣^{2} < ε^{2}$ , and [A5] gives $∥ x - s_{n} ∥^{2} = ∥ x - P_{E_{n}} x ∥^{2} = \sum_{i \in I ∖ E_{n}} ∣ a_{i} ∣^{2} < ε^{2}$ . Hence $∥ x - s_{n} ∥ < ε$ for every $n \geq n_{0}$ , that is, $s_{n} \to x$ .

step 1.3A5A6

3.1

Claims 1, 2 and 3 are established by steps 1.1, 1.2 and 2.1, so a complete orthonormal family expands every vector uniquely and unconditionally in norm.

step 1.1step 1.2step 2.1∎

Depends on

Used by

The unilateral shift obstructs a cyclic linear trace extension Counterexample
Polar decomposition of the unilateral shift Example
The standard basis of ℓ²(ℕ) Example
Positive square root of a compact positive operator Lemma
A Hilbert space with a given orthonormal basis is ℓ² of the index set Theorem
Fourier series converge in mean square Theorem
Hilbert–Schmidt operators are compact Theorem
L two kernels give Hilbert–Schmidt operators Theorem
Peter–Weyl theorem Theorem
Riesz–Fischer: the Fourier coefficient map is onto the space of square-summable families Theorem
Singular value decomposition for compact operators Theorem
Spectral theorem for compact self adjoint operators Theorem
The Fourier basis and Parseval's identity on the finite torus Theorem
Trace is absolutely convergent and basis independent Theorem

Dependency tree · two levels

53 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.1, pp.49–50, Theorem 2.2 (standard reference, not scraped)
Andrew Lin and Casey Rodriguez, MIT 18.102 Introduction to Functional Analysis, printed pp.72–80 (standard reference, not scraped)