CorollaryStatement: 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.

A separable infinite-dimensional Hilbert space is $ℓ^{2}$

Statement

In ZF, every separable infinite-dimensional real or complex Hilbert space $H$ (Separability: the existence of an at most countable dense subset, Hilbert space) is linearly isometric to $ℓ^{2} (N, F)$ (Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ ): there is a linear bijection $Φ : H \to ℓ^{2} (N, F)$ with $∥ Φ (x) ∥_{2} = ∥ x ∥$ and $⟨ Φ (x), Φ (y) ⟩_{ℓ^{2}} = ⟨ x, y ⟩$ for all $x, y \in H$ .

Here infinite-dimensional means what is used below and nothing more: $H$ is not the linear span of any finite set of vectors. No choice principle is used: one existential dense set and one enumeration witness are instantiated, Gram–Schmidt is deterministic, and only the canonical initial partial sums of the resulting sequence occur.

Facts & Assumptions

[A1]

Separability supplies an at most countable dense subset $D \subseteq H$ , and a nonempty at most countable set is a surjective image of $N$ (Separability: the existence of an at most countable dense subset, A nonempty set is at most countable iff it is a surjective image of $N$ ).

[A2]

Gram–Schmidt applied to a sequence with dense range produces an orthonormal set $L$ with closed linear span $H$ , enumerated canonically by the stages of the recursion; the enumeration is a bijection of an infinite subset of $N$ , hence a bijection onto $N$ when $L$ is infinite (A Hilbert space with a dense sequence has a finite or countable orthonormal basis, Every subset of an at most countable set is at most countable).

[A3]

If $S = {e_{0}, \dots, e_{m - 1}}$ is a finite orthonormal set whose closed linear span is $H$ , fix $x \in H$ , put $p = \sum_{j < m} ⟨ x, e_{j} ⟩ e_{j} \in span S$ , and set $w = x - p$ . Finite orthonormal expansion makes $w ⊥ S$ , hence $w ⊥ span S$ . If $w \neq 0$ , then for every $y \in span S$ , Cauchy–Schwarz gives $∥ x - y ∥ ∥ w ∥ \geq ∣ ⟨ x - y, w ⟩ ∣ = ∥ w ∥^{2}$ , so the ball of radius $∥ w ∥ / 2$ about $x$ misses $span S$ , contradicting $x \in \overline{span S} = H$ . Thus $w = 0$ , so $x = p \in span S$ and $H$ is spanned by finitely many vectors. This closure argument chooses no approximating sequence (The finite Bessel inequality and best approximation by a finite orthonormal family, Pythagoras and finite orthogonal sums, Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs).

[A4]

For an orthonormal sequence $(e_{k})_{k \in N}$ with closed linear span $H$ and $x \in H$ , the partial sums $s_{n} = \sum_{k < n} ⟨ x, e_{k} ⟩ e_{k}$ satisfy $∥ x - s_{n} ∥^{2} = ∥ x ∥^{2} - t_{n}$ with $t_{n} = \sum_{k < n} ∣ ⟨ x, e_{k} ⟩ ∣^{2}$ , and $∥ x - s_{n} ∥$ is the distance from $x$ to $span {e_{0}, \dots, e_{n - 1}}$ ; these subspaces increase to the span of the whole sequence, whose distance from $x$ is $0$ because that span is dense (The finite Bessel inequality and best approximation by a finite orthonormal family, The closure of a nonempty $A$ is ${x : d (x, A) = 0}$ , equals $A$ together with its limit points, and is the smallest closed superset, Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets).

[A5]

Every nonincreasing sequence of reals bounded below converges to its infimum, and every nondecreasing sequence of reals bounded above converges to its supremum (A nondecreasing sequence bounded above converges to the supremum of its range, and a nonincreasing sequence bounded below to the infimum).

[A6]

For every finite pairwise orthogonal family $z_{1}, \dots, z_{r}$ , $∥ \sum_{j = 1}^{r} z_{j} ∥^{2} = \sum_{j = 1}^{r} ∥ z_{j} ∥^{2}$ ; a vector of $ℓ^{2} (N, F)$ has finite square sum $T = \sum_{k \in N} ∣ a_{k} ∣^{2} = \sup_{n} t_{n}$ with $t_{n} = \sum_{k < n} ∣ a_{k} ∣^{2}$ , and $H$ is complete for its norm, so a Cauchy sequence in $H$ converges (Pythagoras and finite orthogonal sums, Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ , Hilbert space).

[A7]

The span of a set of vectors is a linear subspace, and an inner product is linear in its first argument (Linear subspace of a vector space, Real and complex inner-product spaces and their induced length).

Proof

technique · direct

Given: A separable infinite-dimensional Hilbert space $H$ over $F$ .

1.1

Choose an at most countable dense set $D \subseteq H$ . Since $H$ is infinite-dimensional it is not spanned by the empty set, so $H \neq {0}$ and $D \neq \emptyset$ ; by [A1] there is a surjection $s : N \to D$ , and the sequence $x_{n} : = s (n)$ has dense range.

A1A7

2.1

Apply Gram–Schmidt to $(x_{n})$ : the resulting orthonormal set $L$ has closed linear span $H$ . The set $L$ must be infinite: otherwise $L$ is finite and [A3] would exhibit $H$ as the span of finitely many vectors, contradicting infinite-dimensionality. Hence the canonical stage enumeration is a bijection of an infinite subset of $N$ onto $L$ , giving an orthonormal sequence $(e_{k})_{k \in N}$ whose closed linear span is $H$ .

step 1.1A2A3

3.1

For $x \in H$ put $t_{n} : = \sum_{k < n} ∣ ⟨ x, e_{k} ⟩ ∣^{2}$ and consider $d_{n} : = ∥ x - \sum_{k < n} ⟨ x, e_{k} ⟩ e_{k} ∥$ . Each $d_{n}$ equals the distance from $x$ to $span {e_{0}, \dots, e_{n - 1}}$ , these subspaces increase with $n$ , and their union is the span of the sequence, which is dense; hence $\inf_{n} d_{n} = 0$ . The sequence $(d_{n})$ is nonincreasing and bounded below, so by [A5] it converges to $0$ ; since $d_{n}^{2} = ∥ x ∥^{2} - t_{n}$ , the sequence $t_{n}$ converges to $∥ x ∥^{2}$ , that is $\sum_{k \in N} ∣ ⟨ x, e_{k} ⟩ ∣^{2} = ∥ x ∥^{2}$ and $\sum_{k < n} ⟨ x, e_{k} ⟩ e_{k} \to x$ .

step 2.1A4A5

3.2

Conversely let $a = (a_{k})_{k \in N} \in ℓ^{2} (N, F)$ and put $σ_{n} : = \sum_{k < n} a_{k} e_{k}$ and $t_{n} : = \sum_{k < n} ∣ a_{k} ∣^{2}$ . For $m \geq n$ Pythagoras gives $∥ σ_{m} - σ_{n} ∥^{2} = t_{m} - t_{n} \leq T - t_{n}$ where $T = \sup_{n} t_{n}$ is finite; by [A5] the nondecreasing bounded sequence $(t_{n})$ converges to $T$ , so the tails $T - t_{n}$ tend to $0$ and $(σ_{n})$ is Cauchy; by completeness it converges to some $S \in H$ . Then $⟨ S, e_{j} ⟩ = a_{j}$ for every $j$ , by continuity of the pairing, and $∥ S ∥^{2} = \sum_{k \in N} ∣ a_{k} ∣^{2}$ .

step 2.1A6A7

4.1

Define $Φ (x) : = (⟨ x, e_{k} ⟩)_{k \in N}$ . By step 3.1 it takes values in $ℓ^{2} (N, F)$ and $∥ Φ (x) ∥_{2} = ∥ x ∥$ ; it is linear by [A7] and injective because $Φ (x) = 0$ forces $∥ x ∥ = 0$ ; by step 3.2 it is surjective, its inverse sending $a$ to the limit $S$ of the partial sums. Inner products are preserved because for finite $n$ one has $⟨ \sum_{k < n} ⟨ x, e_{k} ⟩ e_{k}, \sum_{k < n} ⟨ y, e_{k} ⟩ e_{k} ⟩ = \sum_{k < n} ⟨ x, e_{k} ⟩ \overline{⟨ y, e_{k} ⟩}$ and both sides converge along $n$ to $⟨ x, y ⟩$ and to the $ℓ^{2}$ pairing of $Φ (x), Φ (y)$ .

step 3.1step 3.2A7

5.1

Therefore $Φ$ is a linear bijection preserving norms and inner products, so the separable infinite-dimensional Hilbert space $H$ is linearly isometric to $ℓ^{2} (N, F)$ in ZF.

step 4.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

81 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, p.52, Theorem 2.6 (standard reference, not scraped)
Andrew Lin and Casey Rodriguez, MIT 18.102 Introduction to Functional Analysis, printed pp.72–80 (standard reference, not scraped)

A separable infinite-dimensional Hilbert space is ℓ2ℓ2