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.1A1

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

1.2A2

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.3A3

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

2.1step 1.3A5A6

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$ .

3.1step 1.1step 1.2step 2.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.

Fourier expansion in a Hilbert space

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources