6.4 All s-numbers equal the singular values in finite dimension
Mathlib defines the singular values of a linear map \(S\) between finite-dimensional Hilbert spaces as \(\sigma _n(S) := \sqrt{\lambda _n(S^* S)}\), where \(\lambda _0 \ge \lambda _1 \ge \dots \) are the eigenvalues of \(S^* S\) in non-increasing order. The following theorem identifies them with every s-number sequence at once.
Let \(H_1, H_2\) be finite-dimensional Hilbert spaces over \(\mathbb {K} \in \{ \mathbb {R}, \mathbb {C}\} \). For every s-number sequence \(s\), every \(S \in \mathcal{L}(H_1, H_2)\) and every \(n \in \mathbb {N}_0\), we have
where \(\sigma _n(S)\) are Mathlib’s eigenvalue-defined singular values.
The Hilbert-space coincidence (Theorem 4.1) reduces \(s_n(S)\) to \(a_n(S)\), so it suffices to identify \(a_n(S)\) with \(\sigma _n(S)\). The operator \(S\) is compact (finite-dimensional domain), so the Schmidt representation (Theorem 6.5) applies and its singular values equal the approximation numbers by Eckart–Young. On the other hand, the eigenvalues of \(S^* S\) are exactly the squares of the Schmidt singular values (with the singular vectors as an eigenbasis), so Mathlib’s \(\sigma _n(S) = \sqrt{\lambda _n(S^* S)}\) coincides with the \(n\)-th Schmidt singular value; for \(n \ge \dim H_1\) both sides vanish.