Singular values of nonnegative diagonal matrices
Abstract
Singular values of nonnegative diagonal matrices.
Theorem 1.1 (Sorting a diagonal spectrum).
Lean statement: D5/S3/Quantum/Schatten/DiagonalSingularValues.singularValuesSorted_diagonal_of_antitone_perm
Proof. Machine-checked in Lean as D5/S3/Quantum/Schatten/DiagonalSingularValues.singularValuesSorted_diagonal_of_antitone_perm (✓ std3). ∎
Citation. Rajendra Bhatia (1997). Matrix Analysis. DOI: 10.1007/978-1-4612-0653-8. URL: https://doi.org/10.1007/978-1-4612-0653-8.
Commentary.
Let a be a nonnegative real vector and σ a permutation for which a∘σ is decreasing. Then the ith decreasing singular value of diag(a) equals aσ(i), with the canonical identification of the finite index types. Repeated entries and zero entries are included.