Singular numbers coincide with all s-numbers (finite dimension)

For operators between finite-dimensional Hilbert spaces, Mathlib's singular numbers LinearMap.singularValues agree with every s-number sequence:

s S n = σₙ(S)    for every s-number sequence s.

Strategy and why

The statement factors through the approximation numbers:

s S n  =  aₙ(S)            (Pietsch uniqueness on Hilbert spaces)
       =  σₙ^{proj}(S)     (Eckart–Young, 'singular values' from the SVD)
       =  σₙ(S)            (Mathlib's eigenvalue-defined singular values)

• Uniqueness (allSNumbers_eq_on_HilbertSpace) gives the first step for every s at once — this is why it suffices to treat aₙ.
• Eckart–Young (SVD.svd_sigma_eq_approx) gives the second step. It depends on the SVD IsCompactOperator.schmidtRepresentation which works in finite dimension.
• The third step σ^{proj} = σ (the project's singular values equal Mathlib's, which are √ of the eigenvalues of S* ∘ S) is project_singularValues_eq. It is proved by diagonalising S* ∘ S (the uₖ are eigenvectors with eigenvalues σₖ²) and matching eigenvalue multiplicities with Mathlib's card_filter_eigenvalues_eq.

Main result

• sn_eq_singularValues_of_finiteDimensional — sₙ = σₙ for every s-number sequence. This is general: specialising s to the approximation numbers gives aₙ = σₙ, so no separate statement is needed.

Eigenvectors of S* ∘ S from the SVD

The SVD expansion S = ∑ σₖ ⟪uₖ, ·⟫ vₖ gives, after collapsing the sum at a basis vector, S uₖ = σₖ vₖ (SVD.svd_apply_left) and dually S* vₖ = σₖ uₖ (svd_adjoint_apply below). Composing, S*∘S uₖ = σₖ² uₖ: the uₖ are eigenvectors of the Gram operator S* ∘ S with eigenvalues σₖ². This is the analytic heart of the coincidence with Mathlib's eigenvalue-defined singular values.

Diagonalisation of the Gram operator and its eigenspaces

theorem SNumbers.project_singularValues_eq {𝕜 : Type u} [RCLike 𝕜] {H₁ H₂ : Type u} [NormedAddCommGroup H₁] [InnerProductSpace 𝕜 H₁] [FiniteDimensional 𝕜 H₁] [NormedAddCommGroup H₂] [InnerProductSpace 𝕜 H₂] [FiniteDimensional 𝕜 H₂] (S : H₁ →L[𝕜] H₂) (n : ℕ) : (↑S).singularValues n = approximationNumber S n

aₙ(S) = σₙ(S): the SVD's singular values are Mathlib's. S is compact (finite-dimensional domain), so the SVD applies and svd_sigma_eq_approx reduces the goal to singularValues S n = σ n. Mathlib defines singularValues as √ of the antitone eigenvalues of S* ∘ S, and svd_eigenvalues_eq_sq shows those eigenvalues are exactly i ↦ σᵢ²; for n < finrank this gives singularValues n = √(σₙ²) = σₙ, and for n ≥ finrank both sides vanish (svd_sigma_eq_zero_of_finrank_le).

theorem SNumbers.sn_eq_singularValues_of_finiteDimensional {𝕜 : Type u} [RCLike 𝕜] {H₁ H₂ : Type u} [NormedAddCommGroup H₁] [InnerProductSpace 𝕜 H₁] [FiniteDimensional 𝕜 H₁] [NormedAddCommGroup H₂] [InnerProductSpace 𝕜 H₂] [FiniteDimensional 𝕜 H₂] {s : Family 𝕜} (hs : IsSNumberSequence fun {X Y : Type u} [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] => s) (S : H₁ →L[𝕜] H₂) (n : ℕ) : s S n = (↑S).singularValues n

Singular numbers coincide with all s-numbers (finite dimension). For every s-number sequence s and operator S between finite-dimensional Hilbert spaces, sₙ(S) = σₙ(S).

Uniqueness reduces sₙ to aₙ (for every s at once), and project_singularValues_eq identifies aₙ with Mathlib's σₙ. Specialising s to the approximation numbers recovers aₙ(S) = σₙ(S), so no separate statement is needed.