6 Singular value decomposition
The singular value decomposition (Schmidt representation) of a compact operator between Hilbert spaces is formalised in BasicResults.SVD, via the singular-value iteration (repeatedly peeling off the top singular pair). The auxiliary class of approximable operators (those whose approximation numbers \(a_n\) tend to zero) and its identification with the compact operators on Hilbert spaces live in the separate AddOns library; this split avoids relying on any approximation-property hypothesis on the underlying space.