Singular values, the two Gram spectra, and the singular system

Mathlib defines the singular values of a linear map A : E →ₗ[𝕜] F between finite-dimensional inner product spaces from the source Gram operator A† A (LinearMap.singularValues). This file shows that the target Gram operator A A† carries the same information: the nonzero eigenvalues of A† A and A A† agree with multiplicity, so their sorted eigenvalue lists agree through the common dimension and vanish beyond the rank of A. Equivalently, A and A† have the same singular values.

The multiplicity statement is Module.End.finrank_eigenspace_comp_comm applied to A and A†. A positive value s occurs among the singular values of A as often as s² occurs among the eigenvalues of A† A (LinearMap.ncard_ofPred_singularValues_eq), and a sorted zero-padded sequence is determined by these multiplicities (Finsupp.eq_of_antitone_of_ncard_eq).

Main declarations

• LinearMap.ncard_ofPred_singularValues_eq: the multiplicity of a positive singular value s is the dimension of the s²-eigenspace of A† A.
• LinearMap.singularValues_adjoint: A† has the same singular values as A.
• LinearMap.sq_singularValues_eq_eigenvalues_self_comp_adjoint: the squared singular values are also the sorted eigenvalues of A A†.
• LinearMap.eigenvalues_adjoint_comp_self_eq_eigenvalues_self_comp_adjoint: the sorted eigenvalues of A† A and A A† agree at every index below both dimensions.
• LinearMap.eigenvalues_adjoint_comp_self_eq_zero_iff, LinearMap.eigenvalues_self_comp_adjoint_eq_zero_iff: both sorted eigenvalue lists vanish exactly from the rank of A on.

The singular system

The second half of the file builds the singular system of A from these spectra. The right singular basis (vᵢ) = A.rightSingularBasis is the ordered orthonormal eigenbasis of A† A, in whose order the singular values are listed (LinearMap.sq_singularValues_fin), and the left singular vectors are uᵢ = σᵢ⁻¹ A vᵢ = A.leftSingularVector i, using total field inversion so that uᵢ = 0 when σᵢ = 0. The singular relations hold at every index, which lets the expansion of A run over the whole basis without splitting off the kernel.

• LinearMap.sq_singularValues_antitone: the squared singular values are nonincreasing.
• LinearMap.sq_singularValues_eq_of_adjoint_comp_self_eigenbasis: any sorted orthonormal Gram eigenbasis recovers the squared singular values, with a zero tail.
• LinearMap.norm_apply_le_of_mem_spanIndices_of_adjoint_comp_self_eigenbasis: an upper bound for ‖A x‖ on a span of Gram eigenvectors with bounded eigenvalues.
• LinearMap.adjoint_comp_self_rightSingularBasis: A† A vᵢ = σᵢ² vᵢ.
• LinearMap.singularValues_eq_single_of_finrank_eq_one: on a one-dimensional source the only singular value is ‖A x‖ for a unit vector x.
• LinearMap.singularValues_mul_norm_le_norm_apply, LinearMap.norm_apply_le_singularValues_mul_norm: σₙ ‖x‖ ≤ ‖A x‖ on the span of the vᵢ with i ≤ n, and ‖A x‖ ≤ σₙ ‖x‖ on the span of the vᵢ with n ≤ i.
• LinearMap.apply_rightSingularBasis: A vᵢ = σᵢ uᵢ.
• LinearMap.adjoint_leftSingularVector: A† uᵢ = σᵢ vᵢ.
• LinearMap.self_comp_adjoint_leftSingularVector: A A† uᵢ = σᵢ² uᵢ.
• LinearMap.orthonormal_leftSingularVector: the uᵢ with σᵢ ≠ 0 are orthonormal.
• LinearMap.sum_norm_inner_leftSingularVector_sq_le: Bessel's inequality for the whole family (uᵢ), zero vectors included.
• LinearMap.apply_eq_sum_singularValues_smul: A x = ∑ᵢ σᵢ ⟪vᵢ, x⟫ uᵢ.
• LinearMap.eq_sum_singularValues_smul_rankOne: A = ∑ᵢ σᵢ uᵢ ⊗ vᵢ, the singular value decomposition in rank-one form.
• LinearMap.exists_orthonormalBasis_apply_eq_leftSingularVector: the nonzero left singular vectors extend, index by index, to an orthonormal basis of the codomain.

Comparison of singular values

The comparison section compares the singular values of two maps with the same source through the Courant–Fischer min–max principle for their source Gram operators.

• LinearMap.singularValues_le_mul_of_norm_apply_le: if ‖B x‖ ≤ c ‖A x‖ for every x, then σᵢ(B) ≤ c σᵢ(A) for every i.
• LinearMap.singularValues_comp_le: if ‖C y‖ ≤ c ‖y‖ for every y, then σᵢ(C A) ≤ c σᵢ(A) for every i.
• LinearMap.singularValues_le_of_norm_apply_le: if ‖A x‖ ≤ c ‖x‖ for every x, with c ≥ 0, then σᵢ(A) ≤ c for every i.
• LinearMap.singularValues_eq_of_norm_apply_eq: if ‖B x‖ = ‖A x‖ for every x, then A and B have the same singular values.
• LinearMap.singularValues_operatorAbs: the modulus |A| = √(A† A) has the same singular values as A.
• LinearMap.singularValues_linearIsometry_comp, LinearMap.singularValues_comp_adjoint_linearIsometry: composing on the left with a linear isometry, or on the right with the adjoint of one, leaves the singular values unchanged.
• LinearMap.singularValues_linearIsometryEquiv_comp, LinearMap.singularValues_comp_linearIsometryEquiv: composing with isometric isomorphisms on either side leaves the singular values unchanged.
• ContinuousLinearMap.singularValues_comp_starProjection_range: an operator into any finite- dimensional inner product space has the same singular values after a range projection as after the corresponding isometric trial map.

Diagonal models

For an orthonormal basis (eᵢ) of E and scalars (dᵢ), the diagonal operator with eᵢ as eigenvectors and diagonal entries dᵢ is Mathlib's Matrix.toLin e.toBasis e.toBasis (Matrix.diagonal d). Its additivity in d (Matrix.diagonal_add), its adjoint (Matrix.toLin_conjTranspose with Matrix.diagonal_conjTranspose) and its symmetry for real entries (Matrix.isSymmetric_toLin_iff) are in Mathlib. The diagonal section computes its singular values and shows that every map is a diagonal map up to isometries on both sides.

• Matrix.toLin_diagonal_apply_self: the diagonal operator sends eᵢ to dᵢ eᵢ.
• Matrix.adjoint_comp_self_toLin_diagonal_apply: the Gram operator sends eᵢ to ‖dᵢ‖² eᵢ.
• OrthonormalBasis.adjoint_comp_self_toLin_diagonal_reindex_apply: the same Gram relation in a reordered diagonal basis.
• Matrix.singularValues_toLin_diagonal: the singular values of the diagonal operator are the norms ‖dᵢ‖ listed in nonincreasing order.
• Matrix.toLin_of_ite_val_eq_apply: the rectangular diagonal map with entries dₖ sends eᵢ to dᵢ fᵢ when i is also an index of (fⱼ), and to 0 otherwise.
• LinearMap.exists_linearIsometryEquiv_eq_comp_toLin_comp: every map A : E →ₗ[𝕜] F is U D V for linear isometric equivalences U of F and V of E and the rectangular diagonal map D with the singular values of A on its diagonal, in any prescribed orthonormal bases.
• LinearMap.exists_linearIsometryEquiv_eq_comp_toLin_diagonal_comp: every endomorphism A is U D V for linear isometric equivalences U, V and the diagonal operator D with the singular values of A as entries, in any prescribed orthonormal basis.
• LinearMap.exists_orthonormal_eq_sum_singularValues_smul_rankOne: the compact singular value decomposition A = ∑_{i < p} σᵢ wᵢ ⊗ vᵢ, with p = min (dim E) (dim F) and both families orthonormal.

Orthogonal-tail bound for bounded maps

The final section transfers the Gram-eigenbasis estimate to bounded maps, supplying the tail bound used in the Eckart–Young and attainment theorems.

• ContinuousLinearMap.norm_comp_orthogonal_spanIndices_le_of_adjoint_comp_self_eigenbasis: the norm on the orthogonal complement of the first n vectors of a sorted Gram eigenbasis is at most the n-th singular value, including indices beyond the source dimension.

Source

The singular-system definitions LinearMap.rightSingularBasis and LinearMap.leftSingularVector are adapted from the AIQ-Kitware DKPS formalization. Original copyright (c) 2026 Kitware, Inc.; Apache-2.0.

References

• R. A. Horn and C. R. Johnson, Matrix Analysis, second edition, Cambridge University Press, 2013, Theorem 1.3.22, Theorem 2.6.3 and Section 7.3.
• R. A. Horn and C. R. Johnson, Topics in Matrix Analysis, Cambridge University Press, 1991, Section 3.3.
• R. Bhatia, Matrix Analysis, Graduate Texts in Mathematics 169, Springer, 1997, Section I.2 (the singular value decomposition).

theorem LinearMap.ncard_ofPred_singularValues_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) {s : ℝ} (hs : 0 < s) : {i : ℕ | T.singularValues i = s}.ncard = Module.finrank 𝕜 ↥(Module.End.eigenspace (adjoint T ∘ₗ T) ↑(s ^ 2))

A positive value s occurs among the singular values of T as many times as the dimension of the s²-eigenspace of T† T.

@[simp]

theorem LinearMap.singularValues_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : (adjoint A).singularValues = A.singularValues

A linear map and its adjoint have the same singular values.

theorem LinearMap.singularValues_of_finrank_le_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {i : ℕ} (hi : Module.finrank 𝕜 F ≤ i) : A.singularValues i = 0

The singular values of A : E →ₗ[𝕜] F vanish from the dimension of the target on.

theorem LinearMap.sum_fin_singularValues {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {M : Type u_4} [AddCommMonoid M] (A : E →ₗ[𝕜] F) (f : ℝ → M) (hf : f 0 = 0) : ∑ i : Fin (Module.finrank 𝕜 E), f (A.singularValues ↑i) = A.singularValues.sum fun (x : ℕ) (s : ℝ) => f s

A sum ∑ᵢ f(σᵢ(A)) over the first dim E singular values is the Finsupp sum of f over all singular values, provided f 0 = 0.

theorem LinearMap.sq_singularValues_eq_eigenvalues_self_comp_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {n : ℕ} (hn : Module.finrank 𝕜 F = n) {i : ℕ} (hin : i < n) : A.singularValues i ^ 2 = ⋯.eigenvalues hn ⟨i, hin⟩

The squared singular values of A are the sorted eigenvalues of the target Gram operator A A†, at every index below the dimension of the target.

theorem LinearMap.eigenvalues_adjoint_comp_self_eq_eigenvalues_self_comp_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {m n : ℕ} (hm : Module.finrank 𝕜 E = m) (hn : Module.finrank 𝕜 F = n) {i : ℕ} (him : i < m) (hin : i < n) : ⋯.eigenvalues hm ⟨i, him⟩ = ⋯.eigenvalues hn ⟨i, hin⟩

The sorted eigenvalues of the source Gram operator A† A and the target Gram operator A A† agree at every index below both dimensions.

theorem LinearMap.eigenvalues_adjoint_comp_self_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {m : ℕ} (hm : Module.finrank 𝕜 E = m) {i : ℕ} (him : i < m) : ⋯.eigenvalues hm ⟨i, him⟩ = 0 ↔ Module.finrank 𝕜 ↥A.range ≤ i

The sorted eigenvalues of the source Gram operator A† A vanish exactly from the rank of A on.

theorem LinearMap.eigenvalues_self_comp_adjoint_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {n : ℕ} (hn : Module.finrank 𝕜 F = n) {i : ℕ} (hin : i < n) : ⋯.eigenvalues hn ⟨i, hin⟩ = 0 ↔ Module.finrank 𝕜 ↥A.range ≤ i

The sorted eigenvalues of the target Gram operator A A† vanish exactly from the rank of A on.

theorem LinearMap.sq_singularValues_antitone {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : Antitone fun (i : ℕ) => A.singularValues i ^ 2

The squared singular values are nonincreasing, including the zero tail.

noncomputable def LinearMap.rightSingularBasis {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : OrthonormalBasis (Fin (Module.finrank 𝕜 E)) 𝕜 E

The right singular basis of A: the orthonormal eigenbasis (vᵢ) of the source Gram operator A† A, ordered so that A† A vᵢ = σᵢ² vᵢ for the singular values σᵢ = A.singularValues i of A, listed in nonincreasing order.

theorem LinearMap.rightSingularBasis_def {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : A.rightSingularBasis = ⋯.eigenvectorBasis ⋯

The right singular basis is Mathlib's ordered eigenbasis of A† A; this connects it to the LinearMap.IsSymmetric.eigenvectorBasis API.

theorem LinearMap.adjoint_comp_self_rightSingularBasis {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (i : Fin (Module.finrank 𝕜 E)) : (adjoint A ∘ₗ A) (A.rightSingularBasis i) = ↑(A.singularValues ↑i ^ 2) • A.rightSingularBasis i

The right singular vectors are eigenvectors of A† A for the squared singular values.

theorem LinearMap.inner_apply_rightSingularBasis {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (i : Fin (Module.finrank 𝕜 E)) (x : E) : inner 𝕜 (A (A.rightSingularBasis i)) (A x) = ↑(A.singularValues ↑i ^ 2) * inner 𝕜 (A.rightSingularBasis i) x

Inner products of A vᵢ against the range of A: ⟪A vᵢ, A x⟫ = σᵢ² ⟪vᵢ, x⟫ for a right singular vector vᵢ.

@[simp]

theorem LinearMap.norm_apply_rightSingularBasis {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (i : Fin (Module.finrank 𝕜 E)) : ‖A (A.rightSingularBasis i)‖ = A.singularValues ↑i

A stretches the i-th right singular vector by the i-th singular value: ‖A vᵢ‖ = σᵢ.

theorem LinearMap.singularValues_eq_single_of_finrank_eq_one {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (hE : Module.finrank 𝕜 E = 1) {x : E} (hx : ‖x‖ = 1) : A.singularValues = Finsupp.single 0 ‖A x‖

On a one-dimensional source, the singular values of A are ‖A x‖ for any unit vector x, followed by zeros.

@[simp]

theorem LinearMap.apply_rightSingularBasis_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {i : Fin (Module.finrank 𝕜 E)} : A (A.rightSingularBasis i) = 0 ↔ A.singularValues ↑i = 0

A right singular vector lies in the kernel of A exactly when its singular value vanishes.

theorem LinearMap.singularValues_mul_norm_le_norm_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {n : ℕ} {x : E} (hx : x ∈ A.rightSingularBasis.spanIndices {i : Fin (Module.finrank 𝕜 E) | ↑i ≤ n}) : A.singularValues n * ‖x‖ ≤ ‖A x‖

On the span of the right singular vectors vᵢ with i ≤ n, A stretches every vector by at least the n-th singular value: σₙ ‖x‖ ≤ ‖A x‖.

theorem LinearMap.norm_apply_le_of_mem_spanIndices_of_adjoint_comp_self_eigenbasis {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {m : ℕ} (e : OrthonormalBasis (Fin m) 𝕜 E) {μ : Fin m → ℝ} (he : ∀ (i : Fin m), (adjoint A ∘ₗ A) (e i) = ↑(μ i) • e i) {s : Set (Fin m)} {c : ℝ} (hc : 0 ≤ c) (hμ : ∀ i ∈ s, μ i ≤ c ^ 2) {x : E} (hx : x ∈ e.spanIndices s) : ‖A x‖ ≤ c * ‖x‖

An upper bound on the Gram eigenvalues of a selected span bounds the norm of A there.

theorem LinearMap.sq_singularValues_eq_of_adjoint_comp_self_eigenbasis {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {m : ℕ} (e : OrthonormalBasis (Fin m) 𝕜 E) {μ : Fin m → ℝ} (hμ : Antitone μ) (he : ∀ (i : Fin m), (adjoint A ∘ₗ A) (e i) = ↑(μ i) • e i) (k : Fin m) : A.singularValues ↑k ^ 2 = μ k

A sorted orthonormal eigenbasis of the Gram operator computes the squared singular values.

theorem LinearMap.norm_apply_le_singularValues_mul_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {n : ℕ} {x : E} (hx : x ∈ A.rightSingularBasis.spanIndices {i : Fin (Module.finrank 𝕜 E) | n ≤ ↑i}) : ‖A x‖ ≤ A.singularValues n * ‖x‖

On the span of the right singular vectors vᵢ with n ≤ i, A stretches every vector by at most the n-th singular value: ‖A x‖ ≤ σₙ ‖x‖.

theorem LinearMap.inv_mul_smul_apply_rightSingularBasis {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (i : Fin (Module.finrank 𝕜 E)) : ((↑(A.singularValues ↑i ^ 2))⁻¹ * ↑(A.singularValues ↑i ^ 2)) • A (A.rightSingularBasis i) = A (A.rightSingularBasis i)

A right singular vector with singular value zero lies in the kernel, so A vᵢ is fixed by the scalar σᵢ⁻² σᵢ² (with total field inversion) even when σᵢ = 0.

noncomputable def LinearMap.leftSingularVector {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (i : Fin (Module.finrank 𝕜 E)) : F

The left singular vectors of A: uᵢ = σᵢ⁻¹ A vᵢ for the right singular basis (vᵢ), with total field inversion, so that uᵢ = 0 when σᵢ = 0. The vectors with σᵢ ≠ 0 form an orthonormal family (LinearMap.orthonormal_leftSingularVector).

theorem LinearMap.leftSingularVector_def {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (i : Fin (Module.finrank 𝕜 E)) : A.leftSingularVector i = (↑(A.singularValues ↑i))⁻¹ • A (A.rightSingularBasis i)

Unfolds the left singular vector uᵢ = σᵢ⁻¹ A vᵢ.

theorem LinearMap.apply_rightSingularBasis {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (i : Fin (Module.finrank 𝕜 E)) : A (A.rightSingularBasis i) = ↑(A.singularValues ↑i) • A.leftSingularVector i

The singular relation A vᵢ = σᵢ uᵢ, valid at every index, including those with σᵢ = 0.

theorem LinearMap.inner_leftSingularVector {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (i j : Fin (Module.finrank 𝕜 E)) : inner 𝕜 (A.leftSingularVector i) (A.leftSingularVector j) = if i = j ∧ A.singularValues ↑i ≠ 0 then 1 else 0

The left singular vectors are orthonormal up to the zero vectors at the vanishing singular values: ⟪uᵢ, uⱼ⟫ is 1 if i = j and σᵢ ≠ 0, and 0 otherwise.

theorem LinearMap.orthonormal_leftSingularVector {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : Orthonormal 𝕜 fun (i : { i : Fin (Module.finrank 𝕜 E) // A.singularValues ↑i ≠ 0 }) => A.leftSingularVector ↑i

The left singular vectors with nonzero singular value form an orthonormal family.

@[simp]

theorem LinearMap.leftSingularVector_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {i : Fin (Module.finrank 𝕜 E)} : A.leftSingularVector i = 0 ↔ A.singularValues ↑i = 0

A left singular vector vanishes exactly when its singular value does.

theorem LinearMap.norm_leftSingularVector_le_one {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (i : Fin (Module.finrank 𝕜 E)) : ‖A.leftSingularVector i‖ ≤ 1

A left singular vector has norm at most one: it is a unit vector when its singular value is nonzero and zero otherwise.

theorem LinearMap.sum_norm_inner_leftSingularVector_sq_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (x : F) : ∑ i : Fin (Module.finrank 𝕜 E), ‖inner 𝕜 (A.leftSingularVector i) x‖ ^ 2 ≤ ‖x‖ ^ 2

Bessel's inequality for the left singular vectors: ∑ᵢ ‖⟪uᵢ, x⟫‖² ≤ ‖x‖². The vectors at the vanishing singular values are zero, so the orthonormal subfamily carries the whole sum.

@[simp]

theorem LinearMap.adjoint_leftSingularVector {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (i : Fin (Module.finrank 𝕜 E)) : (adjoint A) (A.leftSingularVector i) = ↑(A.singularValues ↑i) • A.rightSingularBasis i

The adjoint singular relation A† uᵢ = σᵢ vᵢ, valid at every index, including those with σᵢ = 0.

theorem LinearMap.self_comp_adjoint_leftSingularVector {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (i : Fin (Module.finrank 𝕜 E)) : (A ∘ₗ adjoint A) (A.leftSingularVector i) = ↑(A.singularValues ↑i ^ 2) • A.leftSingularVector i

The eigenvalue equation A A† uᵢ = σᵢ² uᵢ for the target Gram operator, at every index. When σᵢ ≠ 0, uᵢ is an eigenvector of A A† for σᵢ²; when σᵢ = 0, uᵢ = 0.

theorem LinearMap.apply_eq_sum_singularValues_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (x : E) : A x = ∑ i : Fin (Module.finrank 𝕜 E), ↑(A.singularValues ↑i) • inner 𝕜 (A.rightSingularBasis i) x • A.leftSingularVector i

The singular expansion of a vector: A x = ∑ᵢ σᵢ ⟪vᵢ, x⟫ uᵢ.

theorem LinearMap.eq_sum_singularValues_smul_rankOne {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : A = ∑ i : Fin (Module.finrank 𝕜 E), ↑(A.singularValues ↑i) • ↑(((InnerProductSpace.rankOne 𝕜) (A.leftSingularVector i)) (A.rightSingularBasis i))

The singular value decomposition in rank-one form: A = ∑ᵢ σᵢ uᵢ ⊗ vᵢ, where u ⊗ v is the rank-one map x ↦ ⟪v, x⟫ u.

theorem LinearMap.exists_orthonormalBasis_apply_eq_leftSingularVector {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : ∃ (w : OrthonormalBasis (Fin (Module.finrank 𝕜 F)) 𝕜 F), ∀ (i : Fin (Module.finrank 𝕜 E)) (j : Fin (Module.finrank 𝕜 F)), ↑i = ↑j → A.singularValues ↑i ≠ 0 → w j = A.leftSingularVector i

The left singular vectors with nonzero singular value extend to an orthonormal basis of the codomain, indexed compatibly with the right singular basis: there is an orthonormal basis (wⱼ) of F with wᵢ = uᵢ whenever σᵢ ≠ 0. Together with LinearMap.apply_rightSingularBasis this gives A vᵢ = σᵢ wᵢ at every index below both dimensions.

theorem LinearMap.singularValues_le_mul_of_norm_apply_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 G] {A : E →ₗ[𝕜] F} {B : E →ₗ[𝕜] G} {c : ℝ} (h : ∀ (x : E), ‖B x‖ ≤ c * ‖A x‖) (i : ℕ) : B.singularValues i ≤ c * A.singularValues i

If ‖B x‖ ≤ c * ‖A x‖ for every x, then every singular value of B is at most c times the corresponding singular value of A.

theorem LinearMap.singularValues_comp_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 G] (C : F →ₗ[𝕜] G) (A : E →ₗ[𝕜] F) {c : ℝ} (hC : ∀ (y : F), ‖C y‖ ≤ c * ‖y‖) (i : ℕ) : (C ∘ₗ A).singularValues i ≤ c * A.singularValues i

Bounded-factor domination. If ‖C y‖ ≤ c * ‖y‖ for every y (for c ≥ 0: if C has operator norm at most c), then σᵢ(C A) ≤ c σᵢ(A) for every i.

theorem LinearMap.singularValues_le_of_norm_apply_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {A : E →ₗ[𝕜] F} {c : ℝ} (hc : 0 ≤ c) (h : ∀ (x : E), ‖A x‖ ≤ c * ‖x‖) (i : ℕ) : A.singularValues i ≤ c

If ‖A x‖ ≤ c * ‖x‖ for every x (for c ≥ 0: if A has operator norm at most c), then every singular value of A is at most c.

theorem LinearMap.singularValues_eq_of_norm_apply_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 G] {A : E →ₗ[𝕜] F} {B : E →ₗ[𝕜] G} (h : ∀ (x : E), ‖B x‖ = ‖A x‖) : B.singularValues = A.singularValues

Two maps with the same source and ‖B x‖ = ‖A x‖ for every x have the same singular values.

@[simp]

theorem LinearMap.singularValues_operatorAbs {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : A.operatorAbs.singularValues = A.singularValues

The modulus |A| = √(A† A) of a map has the same singular values as the map itself.

@[simp]

theorem LinearMap.singularValues_linearIsometry_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 G] (W : F →ₗᵢ[𝕜] G) (A : E →ₗ[𝕜] F) : (W.toLinearMap ∘ₗ A).singularValues = A.singularValues

Composing on the left with a linear isometry leaves the singular values unchanged.

@[simp]

theorem LinearMap.singularValues_comp_adjoint_linearIsometry {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 G] (A : E →ₗ[𝕜] F) (W : E →ₗᵢ[𝕜] G) : (A ∘ₗ adjoint W.toLinearMap).singularValues = A.singularValues

Composing on the right with the adjoint of a linear isometry leaves the singular values unchanged.

@[simp]

theorem LinearMap.singularValues_linearIsometryEquiv_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 G] (U : F ≃ₗᵢ[𝕜] G) (A : E →ₗ[𝕜] F) : (↑↑↑U ∘ₗ A).singularValues = A.singularValues

Composing on the left with an isometric isomorphism leaves the singular values unchanged.

@[simp]

theorem LinearMap.singularValues_comp_linearIsometryEquiv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 G] (A : E →ₗ[𝕜] F) (V : G ≃ₗᵢ[𝕜] E) : (A ∘ₗ ↑↑↑V).singularValues = A.singularValues

Composing on the right with an isometric isomorphism leaves the singular values unchanged.

@[simp]

theorem LinearMap.singularValues_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (c : 𝕜) (A : E →ₗ[𝕜] F) : (c • A).singularValues = ‖c‖ • A.singularValues

Scaling a map by c scales its singular values by ‖c‖.

@[simp]

theorem Matrix.toLin_diagonal_apply_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (e : OrthonormalBasis ι 𝕜 E) (d : ι → 𝕜) (i : ι) : ((toLin e.toBasis e.toBasis) (diagonal d)) (e i) = d i • e i

The diagonal operator of an orthonormal basis (eᵢ) with entries (dᵢ) has eᵢ as an eigenvector with eigenvalue dᵢ.

@[simp]

theorem Matrix.adjoint_comp_self_toLin_diagonal_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (e : OrthonormalBasis ι 𝕜 E) (d : ι → 𝕜) (i : ι) : have this := ⋯; have D := (toLin e.toBasis e.toBasis) (diagonal d); (LinearMap.adjoint D ∘ₗ D) (e i) = ↑(‖d i‖ ^ 2) • e i

The Gram operator of a diagonal map has eigenvalues equal to the squared diagonal norms.

theorem OrthonormalBasis.adjoint_comp_self_toLin_diagonal_reindex_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (e : OrthonormalBasis ι 𝕜 E) (d : ι → 𝕜) {κ : Type u_5} [Fintype κ] (π : κ ≃ ι) (i : κ) : have this := ⋯; have D := (Matrix.toLin e.toBasis e.toBasis) (Matrix.diagonal d); (LinearMap.adjoint D ∘ₗ D) ((e.reindex π.symm) i) = ↑(‖d (π i)‖ ^ 2) • (e.reindex π.symm) i

Reindexing a diagonal basis preserves the Gram eigenvector equations, with the squared diagonal norms reindexed by the same equivalence.

theorem Matrix.singularValues_toLin_diagonal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (e : OrthonormalBasis ι 𝕜 E) (d : ι → 𝕜) {n : ℕ} (π : Fin n ≃ ι) (hπ : Antitone fun (k : Fin n) => ‖d (π k)‖) (k : Fin n) : ((toLin e.toBasis e.toBasis) (diagonal d)).singularValues ↑k = ‖d (π k)‖

Singular values of a diagonal operator. If π lists the indices so that the norms ‖d (π k)‖ are nonincreasing, then the k-th singular value of the diagonal operator with entries d in an orthonormal basis is ‖d (π k)‖. The singular values from Fintype.card ι on vanish (LinearMap.singularValues_of_finrank_le).

theorem Matrix.toLin_of_ite_val_eq_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {m n : ℕ} (e : OrthonormalBasis (Fin m) 𝕜 E) (f : OrthonormalBasis (Fin n) 𝕜 F) (d : ℕ → 𝕜) (i : Fin m) : ((toLin e.toBasis f.toBasis) (of fun (j : Fin n) (i : Fin m) => if ↑j = ↑i then d ↑i else 0)) (e i) = if h : ↑i < n then d ↑i • f ⟨↑i, h⟩ else 0

The rectangular diagonal map with entries d in orthonormal bases (eᵢ)_{i < m} and (fⱼ)_{j < n} sends eᵢ to dᵢ fᵢ when i < n, and to 0 otherwise.

theorem LinearMap.exists_linearIsometryEquiv_eq_comp_toLin_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {m n : ℕ} (e : OrthonormalBasis (Fin m) 𝕜 E) (f : OrthonormalBasis (Fin n) 𝕜 F) : ∃ (U : F ≃ₗᵢ[𝕜] F) (V : E ≃ₗᵢ[𝕜] E), A = ↑↑↑U ∘ₗ (Matrix.toLin e.toBasis f.toBasis) (Matrix.of fun (j : Fin n) (i : Fin m) => if ↑j = ↑i then ↑(A.singularValues ↑i) else 0) ∘ₗ ↑↑↑V

Rectangular singular-value factorization. Every linear map A : E →ₗ[𝕜] F between finite-dimensional inner product spaces factors as A = U D V, where U and V are linear isometric equivalences of F and E, and D is the rectangular diagonal map whose matrix in prescribed orthonormal bases (eᵢ) of E and (fⱼ) of F has the singular values of A on its diagonal: D eᵢ = σᵢ fᵢ when i is also an index of (fⱼ), and D eᵢ = 0 otherwise.

theorem LinearMap.exists_linearIsometryEquiv_eq_comp_toLin_diagonal_comp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E) {n : ℕ} (e : OrthonormalBasis (Fin n) 𝕜 E) : ∃ (U : E ≃ₗᵢ[𝕜] E) (V : E ≃ₗᵢ[𝕜] E), A = ↑↑↑U ∘ₗ (Matrix.toLin e.toBasis e.toBasis) (Matrix.diagonal fun (i : Fin n) => ↑(A.singularValues ↑i)) ∘ₗ ↑↑↑V

Singular-value diagonal factorization. Every endomorphism A of a finite-dimensional inner product space factors as A = U D V, where U and V are linear isometric equivalences and D is the diagonal operator whose entries in a prescribed orthonormal basis (eᵢ) are the singular values of A.

theorem LinearMap.exists_orthonormal_eq_sum_singularValues_smul_rankOne {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : ∃ (v : Fin (min (Module.finrank 𝕜 E) (Module.finrank 𝕜 F)) → E) (w : Fin (min (Module.finrank 𝕜 E) (Module.finrank 𝕜 F)) → F), Orthonormal 𝕜 v ∧ Orthonormal 𝕜 w ∧ A = ∑ i : Fin (min (Module.finrank 𝕜 E) (Module.finrank 𝕜 F)), ↑(A.singularValues ↑i) • ↑(((InnerProductSpace.rankOne 𝕜) (w i)) (v i))

Compact singular value decomposition. With p = min (dim E) (dim F), every map A : E →ₗ[𝕜] F is ∑_{i < p} σᵢ wᵢ ⊗ vᵢ for orthonormal families (vᵢ) in E and (wᵢ) in F, where u ⊗ v is the rank-one map x ↦ ⟪v, x⟫ u. Unlike LinearMap.eq_sum_singularValues_smul_rankOne, both families are orthonormal, including at the indices where σᵢ = 0.

theorem ContinuousLinearMap.norm_comp_orthogonal_spanIndices_le_of_adjoint_comp_self_eigenbasis {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (T : E →L[𝕜] F) {m : ℕ} (e : OrthonormalBasis (Fin m) 𝕜 E) {μ : Fin m → ℝ} (hμ : Antitone μ) (he : ∀ (i : Fin m), (LinearMap.adjoint ↑T ∘ₗ ↑T) (e i) = ↑(μ i) • e i) (n : ℕ) : ‖T ∘SL (e.spanIndices ↑{i : Fin m | ↑i < n})ᗮ.subtypeL‖ ≤ (↑T).singularValues n

For a sorted orthonormal eigenbasis of T† T, the norm on the orthogonal complement of its first n vectors is at most the n-th singular value, including the zero tail.

theorem ContinuousLinearMap.singularValues_comp_starProjection_range {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 G] {X : F →L[𝕜] E} (hX : Isometry ⇑X) (T : E →L[𝕜] G) : (↑(T ∘SL (↑X).range.starProjection)).singularValues = (↑(T ∘SL X)).singularValues

For an isometry X, an operator T has the same singular values after the projection onto range X as after X itself: T P_{range X} = (T X) X† and X† is the adjoint of an isometry.