TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 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.

Singular value decomposition for compact operators

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H$ and $K$ be real or complex Hilbert spaces (Hilbert space), let $T \in B (H, K)$ be a compact operator (Compact linear operator), let $∣ T ∣$ and the singular values $s_{n} (T)$ be as in the absolute-value definition (Absolute value and singular values of a compact operator). Let $J = {1, 2, 3, \dots}$ when $ran T$ is infinite-dimensional. When $ran T$ is finite-dimensional, put $r : = \dim ran T \in N$ (Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis) and let $J = {1, \dots, r}$ , interpreted as $\emptyset$ when $r = 0$ . Thus $J$ indexes exactly the positive singular values counted with multiplicity, which we write as $(s_{j})_{j \in J}$ in nonincreasing order. Then:

there are orthonormal families $(e_{j})_{j \in J}$ in $(\ker T)^{⊥}$ and $(f_{j})_{j \in J}$ in $\overline{ran T}$ , indexed by exactly $J$ , with $∣ T ∣ e_{j} = s_{j} e_{j}$ and $f_{j} = s_{j}^{- 1} T e_{j}$ for every $j \in J$ ;
for every $x \in H$ the series converges in norm and $T x = \sum_{j \in J} s_{j} ⟨ x, e_{j} ⟩ f_{j},$ and its finite partial sums $T_{n} : = \sum_{j \leq n} s_{j} ⟨ \cdot, e_{j} ⟩ f_{j}$ satisfy $∥ T - T_{n} ∥ \leq s_{n + 1}$ for every $n$ with $n + 1 \in J$ (and $T_{n} = T$ for $n \geq r$ when $r < + \infty$ );
the linear map $U$ defined on the span of ${e_{j} : j \in J}$ by $U e_{j} : = f_{j}$ , extended by continuity to $(\ker T)^{⊥}$ and by zero on $\ker T$ , is a partial isometry with $T = U ∣ T ∣, U^{*} U = P_{(\ker T)^{⊥}}, U^{*} U is the orthogonal projection onto (\ker T)^{⊥},$ and $U U^{*}$ the orthogonal projection onto $\overline{ran T}$ ;
the zero-padded sequence $(s_{n} (T))_{n \geq 1}$ is not used to index the orthonormal systems: the systems carry exactly the index set $J$ of the positive singular values, and the terms $s_{n} (T) = 0$ beyond the rank in the finite-rank case are numerical padding only.

Facts & Assumptions

Given: Countable Choice, compact $T : H \to K$ , its absolute value $∣ T ∣$ , the index set $J$ of the positive singular values with multiplicity, the finite dimension $r = \dim ran T$ when the range is finite-dimensional, and the zero-padded sequence $(s_{n} (T))$ .

[A1]

Absolute value and finite rank. $∣ T ∣$ is compact, self-adjoint and positive with $∣ T ∣^{2} = T^{*} T$ , $∥ ∣ T ∣ x ∥ = ∥ T x ∥$ and $\ker ∣ T ∣ = \ker T$ ; the positive singular values with multiplicity are the positive eigenvalues of $∣ T ∣$ with multiplicity. They are finite in number exactly when $ran T$ is finite-dimensional, and otherwise form a countably infinite list. In the finite-dimensional case the isometric linear bijection $Φ : ran ∣ T ∣ \to ran T$ , $Φ (∣ T ∣ x) = T x$ , gives $\dim ran ∣ T ∣ = \dim ran T = r$ (Absolute value and singular values of a compact operator, Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis). No value $\dim V = \infty$ is used.

[A2]

Spectral theorem for $∣ T ∣$ . The nonzero eigenvalues of $∣ T ∣$ are positive, have finite-dimensional eigenspaces $E_{λ}$ , are mutually orthogonal across distinct $λ$ , and their closed span is $(\ker ∣ T ∣)^{⊥} = \overline{ran ∣ T ∣}$ ; moreover $\ker ∣ T ∣ = \ker T$ and $H = (\ker T)^{⊥} \oplus \ker T$ , so the closed span of the eigenspaces is $(\ker T)^{⊥}$ (Spectral theorem for compact self adjoint operators, Eigenspaces of a self adjoint operator are orthogonal, Eigenvalues, eigenvectors, eigenspaces $E_{λ} (T) = \ker (T - λ I)$ , and the spectrum $σ_{F} (T)$ of an endomorphism, Orthogonality and the orthogonal complement, Orthogonal decomposition by a closed subspace).

[A3]

Bases and expansion. Every finite-dimensional eigenspace $E_{λ}$ has an orthonormal basis (Every finite-dimensional real or complex inner product space has an orthonormal basis); an orthonormal family is complete in a closed subspace in the case, and only in the case, that the finite-subset net of Fourier sums converges there, with Parseval and Bessel inequalities available (Fourier expansion in a Hilbert space, Parseval equivalences for an orthonormal family, The finite Bessel inequality and best approximation by a finite orthonormal family, Orthonormal families, complete orthonormal systems and Hilbert bases).

[A4]

Continuity. Bounded operators are continuous and satisfy $∥ S x ∥ \leq ∥ S ∥ ∥ x ∥$ ; limits are unique (A bounded linear operator between normed spaces, For a linear operator, boundedness, continuity at 0, continuity, and Lipschitz continuity are equivalent, The operator norm as the least bound and as the unit-sphere or unit-ball supremum, Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ ).

[A5]

Countable Choice supplies, for the at most countable eigenvalue list, one orthonormal basis of each finite-dimensional eigenspace (The Axiom of Countable Choice ( ${A C}_{ω}$ ), Finite, countably infinite, countable, uncountable).

Proof

technique · direct

Given: Countable Choice, the compact $T$ , its absolute value $∣ T ∣$ , the index set $J$ and the singular values $s_{j}$ , the finite integer $r$ when $ran T$ is finite-dimensional, and the eigenspaces $E_{λ}$ of $∣ T ∣$ for positive eigenvalues $λ$ .

1.1

Choosing the left system. By [A2] the positive eigenvalues of $∣ T ∣$ are precisely the positive singular values with multiplicity, and their eigenspaces are finite-dimensional with closed span $(\ker T)^{⊥}$ ; listing those eigenvalues with multiplicity as $(s_{j})_{j \in J}$ and choosing by [A5] an orthonormal basis of each $E_{λ}$ gives an orthonormal family $(e_{j})_{j \in J}$ with $∣ T ∣ e_{j} = s_{j} e_{j}$ for every $j$ , whose closed linear span is $(\ker T)^{⊥}$ , and the terms $s_{j} > 0$ are in nonincreasing order.

A1A2A3A5

2.1

The right system is orthonormal. For $j \in J$ put $f_{j} : = s_{j}^{- 1} T e_{j}$ , which lies in $ran T \subseteq \overline{ran T}$ and is well defined because $s_{j} > 0$ . For $i, j \in J$ , using $∣ T ∣^{2} = T^{*} T$ and the eigenvector property of [step 1.1], $⟨ f_{i}, f_{j} ⟩ = \frac{1}{s_{i} s_{j}} ⟨ T e_{i}, T e_{j} ⟩ = \frac{1}{s_{i} s_{j}} ⟨ T^{*} T e_{i}, e_{j} ⟩ = \frac{1}{s_{i} s_{j}} ⟨ ∣ T ∣^{2} e_{i}, e_{j} ⟩ = \frac{s_{i}^{2}}{s_{i} s_{j}} ⟨ e_{i}, e_{j} ⟩ = δ_{i j},$ so $(f_{j})_{j \in J}$ is orthonormal.

step 1.1A1

3.1

The expansion. Let $x \in H$ . By [A2] write $x = m + n$ with $m \in (\ker T)^{⊥}$ and $n \in \ker T$ . Since $(e_{j})$ is complete in $(\ker T)^{⊥}$ [step 1.1], the Fourier expansion [A3] gives $m = \sum_{j \in J} ⟨ m, e_{j} ⟩ e_{j} = \sum_{j \in J} ⟨ x, e_{j} ⟩ e_{j}$ as a norm limit of finite-subset partial sums, and then continuity of $T$ [A4] gives $T x = T m = \sum_{j \in J} ⟨ x, e_{j} ⟩ T e_{j} = \sum_{j \in J} s_{j} ⟨ x, e_{j} ⟩ f_{j}$ , because $T n = 0$ and the image net of the finite partial sums converges. Moreover for finite $F \subseteq J$ the remainder is $∥ (T - \sum_{j \in F} s_{j} ⟨ \cdot, e_{j} ⟩ f_{j}) x ∥^{2} = \sum_{j \notin F} s_{j}^{2} ∣ ⟨ x, e_{j} ⟩ ∣^{2} \leq s_{n + 1}^{2} ∥ x ∥^{2}$ whenever $F \supseteq {1, \dots, n}$ , by orthonormality [step 2.1] and Bessel [A3], so the partial sums $T_{n}$ of the statement satisfy $∥ T - T_{n} ∥ \leq s_{n + 1}$ for $n + 1 \in J$ , and $T_{n} = T$ for $n \geq r$ in the finite-rank case because then $s_{j} = 0$ for $j > r$ and every index in $J$ is $\leq r$ .

step 1.1step 2.1A1A3A4

4.1

The right system spans the range closure. Each $f_{j} = s_{j}^{- 1} T e_{j}$ lies in $ran T$ by [step 2.1], so the closed linear span $N : = \overset{}{span} {f_{j} : j \in J}$ is contained in $\overline{ran T}$ ; conversely [step 3.1] exhibits every $T x$ as the norm limit of finite linear combinations of the $f_{j}$ , so $ran T \subseteq N$ and hence $\overline{ran T} = N$ .

step 2.1step 3.1

5.1

The partial isometry and $T = U ∣ T ∣$ . Define $U$ first on the linear span $V$ of ${e_{j} : j \in J}$ by $U (\sum_{j \in F} c_{j} e_{j}) : = \sum_{j \in F} c_{j} f_{j}$ for finite $F$ . This is well defined because $(e_{j})$ is linearly independent as an orthonormal family, and it is isometric, since by [step 2.1] $∥ \sum c_{j} f_{j} ∥^{2} = \sum ∣ c_{j} ∣^{2} = ∥ \sum c_{j} e_{j} ∥^{2}$ ; by [step 1.1] the closure of $V$ is $(\ker T)^{⊥}$ , so $U$ extends uniquely to a bounded linear operator, still denoted $U$ , on $(\ker T)^{⊥}$ with $∥ U m ∥ = ∥ m ∥$ for all $m \in (\ker T)^{⊥}$ and $U ((\ker T)^{⊥}) = \overset{}{span} {f_{j}} = \overline{ran T}$ by [step 4.1]. Extend $U$ to $H = (\ker T)^{⊥} \oplus \ker T$ by $U = 0$ on $\ker T$ ; then $U$ is bounded and, because $∣ T ∣$ is self-adjoint with $∣ T ∣ e_{j} = s_{j} e_{j}$ , $U ∣ T ∣ e_{j} = U s_{j} e_{j} = s_{j} f_{j} = T e_{j}$ for every $j$ and $U ∣ T ∣ = 0 = T$ on $\ker T = ∣ T ∣^{- 1} (0)$ [A1], so $U ∣ T ∣ = T$ by continuity on the closed span of $\ker T$ and the $e_{j}$ , which is $H$ by [A2]. Finally $U^{*} U$ and $U U^{*}$ : for $x, y \in H$ one has $⟨ U x, U y ⟩ = ⟨ P x, P y ⟩$ where $P$ is the orthogonal projection onto $(\ker T)^{⊥}$ , because $U$ is isometric on $(\ker T)^{⊥}$ and vanishes on $\ker T$ , so $⟨ U^{*} U x, y ⟩ = ⟨ P x, y ⟩$ and $U^{*} U = P$ ; dually, for $y \in K$ the vector $U^{*} y \in (\ker T)^{⊥}$ is characterised by $⟨ U^{*} y, z ⟩ = ⟨ y, U z ⟩$ for all $z \in (\ker T)^{⊥}$ , so $U U^{*} y = y$ for $y \in \overline{ran T}$ and $U U^{*} y = 0$ for $y ⊥ \overline{ran T}$ , that is $U U^{*}$ is the orthogonal projection onto $\overline{ran T}$ .

step 1.1step 2.1step 4.1A1A2A4

6.1

Conclusion. Claim 1 is [step 1.1] and [step 2.1]; claim 2 is [step 3.1], whose index set is $J$ by construction; claim 3 is [step 5.1] together with [step 4.1]. Claim 4 is the indexing discipline used throughout: $J$ indexes the positive singular values with multiplicity and is $\emptyset$ only for $T = 0$ , when the finite dimension is $r = 0$ ; it is finite exactly when the range is finite-dimensional. In that case the vanishing terms $s_{n} (T) = 0$ with $n > r$ are numerical padding and index no vector.

step 1.1step 2.1step 3.1step 4.1step 5.1A1∎

Depends on

Used by

Compact operator iff approximation numbers tend to zero Corollary
Finite rank operators are norm dense in compact Hilbert space operators Corollary
Trace class operator Definition
Trace of a trace class operator Definition
Adjoint, norm and trace of an operator of rank at most one Example
Nuclear series characterizes trace norm Lemma
Singular values equal approximation numbers Lemma
Schatten p classes Remark
Cyclicity of the trace Theorem
Trace class iff product of two Hilbert Schmidt operators Theorem
Trace is absolutely convergent and basis independent Theorem
Trace of a positive operator is the sum of its eigenvalues Theorem

Dependency tree · two levels

121 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 — §3.5, Theorem 3.17 (printed pp. 90–92) (standard reference, not scraped)
Anthony W. Knapp, Advanced Real Analysis — Chapter II, §§4–5 (standard reference, not scraped)