Singular value decomposition of a Hilbert-space operator

A non-negative real σ is a singular value of S : H₁ →L[𝕜] H₂ if there is a singular vector pair (u, v): unit vectors u ∈ H₁, v ∈ H₂ with S u = σ • v and S* v = σ • u.

This file develops the SVD of a compact operator via the singular-value iteration (peeling off the top singular pair given by norm_isSingularValue), and the scalar factorisation for general operators.

Main results

• SVD.IsCompactOperator.norm_isSingularValue — every compact operator attains its operator norm as a singular value.
• SVD.IsCompactOperator.schmidtRepresentation — the singular value decomposition / Schmidt representation S x = Σ aₖ ⟨uₖ,x⟩ vₖ. Needs the infinite iteration plus the convergence facts σₖ → 0, HasSum.
• SVD.IsCompactOperator.truncation_residual_eq_approxNumber — Eckart–Young ‖S - Sₙ‖ = aₙ(S), identifying singular values with approximation numbers.
• SVD.IsCompactOperator.diagonalFactorisation — the factorisation B ∘ S ∘ A = diag(a₀, …, aₙ) through ℓ₂ⁿ⁺¹. Needs only the top n+1 singular pairs — a finite truncation that (pinning the exact aₖ) requires S compact.
• SVD.exists_scalar_factorisation — B ∘ S ∘ A = c • id for c < aₙ(S), for an arbitrary bounded S.
• SVD.mul_approximationNumber_le_of_factorization — for a compact T = T₂T₁, (n+1)·aₙ(T) ≤ ‖T₁‖_HS·‖T₂‖_HS (Pietsch 2.11.23), with the two Hilbert–Schmidt norms entering only as hypothesised bounds on ∑ₖ ‖T₁ uₖ‖² and ∑ₖ ‖T₂* vₖ‖², so that no Schatten-class theory is needed; SVD.sum_norm_sq_apply_le_of_rows derives such a bound from the rows of an operator (Bessel plus a row bound).

Orthonormal-or-zero families

The SVD below is indexed by ℕ, but a genuinely ℕ-indexed Orthonormal family cannot exist in a finite-dimensional space. We therefore index the SVD by the finite-dimension-compatible relaxation OrthonormalOrZero: each vector is a unit vector or zero, and distinct vectors are orthogonal. In a finite-dimensional space all but finitely many vectors are zero (those with singular value 0), so the family genuinely exists; Orthonormal is the special case with no zeros.

def SVD.OrthonormalOrZero (𝕜 : Type u_1) [RCLike 𝕜] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {ι : Type u_3} (u : ι → H) : Prop

OrthonormalOrZero 𝕜 u: each u i is a unit vector or zero, and distinct vectors are orthogonal.

Equations

• SVD.OrthonormalOrZero 𝕜 u = ((∀ (i : ι), ‖u i‖ = 1 ∨ u i = 0) ∧ Pairwise fun (i j : ι) => inner 𝕜 (u i) (u j) = 0)

theorem Orthonormal.orthonormalOrZero {𝕜 : Type u} [RCLike 𝕜] {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {ι : Type u_2} {u : ι → H} (hu : Orthonormal 𝕜 u) : SVD.OrthonormalOrZero 𝕜 u

Orthonormal families are OrthonormalOrZero.

theorem SVD.OrthonormalOrZero.inner_eq {𝕜 : Type u} [RCLike 𝕜] {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {ι : Type u_2} [DecidableEq ι] {u : ι → H} (h : OrthonormalOrZero 𝕜 u) (i j : ι) : inner 𝕜 (u i) (u j) = if i = j then ↑‖u i‖ ^ 2 else 0

Inner products of an orthonormal-or-zero family: ⟪uᵢ, uⱼ⟫ = δᵢⱼ ‖uᵢ‖² (with ‖uᵢ‖² ∈ {0, 1}).

theorem SVD.OrthonormalOrZero.orthonormal_comp {𝕜 : Type u} [RCLike 𝕜] {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {ι : Type u_2} {κ : Type u_3} {u : ι → H} (h : OrthonormalOrZero 𝕜 u) {g : κ → ι} (hg : Function.Injective g) (hn : ∀ (k : κ), ‖u (g k)‖ = 1) : Orthonormal 𝕜 fun (k : κ) => u (g k)

Restricting away the zeros. An OrthonormalOrZero family, reindexed along an injective map that only hits unit vectors, is Orthonormal. This is how a finite subfamily of an SVD family — the indices with non-zero singular value — is recognised as an orthonormal basis of its span.

theorem SVD.OrthonormalOrZero.norm_sum_smul_sq {𝕜 : Type u} [RCLike 𝕜] {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {ι : Type u_2} {u : ι → H} (h : OrthonormalOrZero 𝕜 u) (c : ι → 𝕜) (s : Finset ι) : ‖∑ k ∈ s, c k • u k‖ ^ 2 = ∑ k ∈ s, ‖c k‖ ^ 2 * ‖u k‖ ^ 2

Finite Pythagoras for an orthonormal-or-zero family: ‖∑ cₖ • uₖ‖² = ∑ ‖cₖ‖² ‖uₖ‖² (zero vectors drop out).

theorem SVD.OrthonormalOrZero.smul_inner_eq {𝕜 : Type u} [RCLike 𝕜] {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {u : ℕ → H} (h : OrthonormalOrZero 𝕜 u) {σ : ℕ → ℝ} (htie : ∀ (k : ℕ), σ k ≠ 0 → u k ≠ 0) (j k : ℕ) : ↑(σ j) * inner 𝕜 (u j) (u k) = if j = k then ↑(σ k) else 0

The σ-weighted inner product of an orthonormal-or-zero family collapses to a Kronecker delta: σⱼ·⟪uⱼ, uₖ⟫ = δⱼₖ·σₖ, given the tie uₖ = 0 ↔ σₖ = 0 (so that a zero vector carries a zero weight, and a nonzero one is unit).

theorem SVD.OrthonormalOrZero.norm_sum_smul_sq_of_support {𝕜 : Type u} [RCLike 𝕜] {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {ι : Type u_2} {u : ι → H} (h : OrthonormalOrZero 𝕜 u) (c : ι → 𝕜) (s : Finset ι) (hc : ∀ k ∈ s, u k = 0 → c k = 0) : ‖∑ k ∈ s, c k • u k‖ ^ 2 = ∑ k ∈ s, ‖c k‖ ^ 2

Finite Pythagoras, weighted form: if the coefficient vanishes wherever the vector does (uₖ = 0 → cₖ = 0), the zero vectors drop and we recover the clean ‖∑ cₖ • uₖ‖² = ∑ ‖cₖ‖².

theorem SVD.OrthonormalOrZero.comp {𝕜 : Type u} [RCLike 𝕜] {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {ι : Type u_2} {κ : Type u_3} {u : ι → H} (h : OrthonormalOrZero 𝕜 u) {f : κ → ι} (hf : Function.Injective f) : OrthonormalOrZero 𝕜 (u ∘ f)

Reindexing an orthonormal-or-zero family by an injection stays orthonormal-or-zero.

theorem SVD.OrthonormalOrZero.sum_inner_products_le {𝕜 : Type u} [RCLike 𝕜] {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {ι : Type u_2} {u : ι → H} (h : OrthonormalOrZero 𝕜 u) (x : H) (s : Finset ι) : ∑ k ∈ s, ‖inner 𝕜 (u k) x‖ ^ 2 ≤ ‖x‖ ^ 2

Bessel's inequality for an orthonormal-or-zero family: ∑ ‖⟪uₖ, x⟫‖² ≤ ‖x‖². Proof via the partial projection p := ∑ ⟪uₖ,x⟫·uₖ: ‖p‖² = ∑‖⟪uₖ,x⟫‖² = re⟪p, x⟫ ≤ ‖p‖·‖x‖, hence ‖p‖ ≤ ‖x‖.

def SVD.IsSingularValue {𝕜 : Type u} [RCLike 𝕜] {H₁ H₂ : Type u} [NormedAddCommGroup H₁] [InnerProductSpace 𝕜 H₁] [CompleteSpace H₁] [NormedAddCommGroup H₂] [InnerProductSpace 𝕜 H₂] [CompleteSpace H₂] (S : H₁ →L[𝕜] H₂) (σ : ℝ) : Prop

A non-negative real σ is a singular value of S if there exist unit vectors u ∈ H₁, v ∈ H₂ with S u = σ • v and S* v = σ • u.

Equations

• SVD.IsSingularValue S σ = ∃ (u : H₁) (v : H₂), ‖u‖ = 1 ∧ ‖v‖ = 1 ∧ S u = ↑σ • v ∧ (ContinuousLinearMap.adjoint S) v = ↑σ • u

theorem SVD.IsCompactOperator.norm_isSingularValue {𝕜 : Type u} [RCLike 𝕜] {H₁ H₂ : Type u} [NormedAddCommGroup H₁] [InnerProductSpace 𝕜 H₁] [CompleteSpace H₁] [NormedAddCommGroup H₂] [InnerProductSpace 𝕜 H₂] [CompleteSpace H₂] [Nontrivial H₁] [Nontrivial H₂] {S : H₁ →L[𝕜] H₂} (hS : IsCompactOperator ⇑S) : IsSingularValue S ‖S‖

Every compact operator between Hilbert spaces attains its norm as a singular value: there exist unit vectors u, v with S u = ‖S‖ • v and S* v = ‖S‖ • u.

Proof sketch: take a maximising sequence xₙ (unit, ‖S xₙ‖ → ‖S‖), extract a strongly convergent subsequence S xₙₖ → y by compactness, let v := ‖S‖⁻¹ • y and u' := S* v. Cauchy–Schwarz on ⟨u', xₙₖ⟩ = ⟨v, S xₙₖ⟩ → ‖S‖ shows ‖u'‖ = ‖S‖; equality in C–S forces xₙₖ → ‖S‖⁻¹ • u' =: u, so by continuity S u = y = ‖S‖ • v.

The Schmidt iteration

svdState S hS n carries the n-th deflated operator Sₙ together with a proof it is still compact (S₀ = S; Sₙ₊₁ = Sₙ - ⟪uₙ, ·⟫ (σₙ • vₙ), where (uₙ, vₙ) attain σₙ = ‖Sₙ‖ as a singular value, norm_isSingularValue). The projections svdT/svdU/svdV read off Sₙ, uₙ, vₙ.

Step properties of the iteration

Orthogonality (the variational step)

Telescoping and the full-operator relations

Orthogonality of the right singular vectors (the adjoint side)

The singular values tend to zero

theorem SVD.IsCompactOperator.schmidtRepresentation {𝕜 : Type u} [RCLike 𝕜] {H₁ H₂ : Type u} [NormedAddCommGroup H₁] [InnerProductSpace 𝕜 H₁] [CompleteSpace H₁] [NormedAddCommGroup H₂] [InnerProductSpace 𝕜 H₂] [CompleteSpace H₂] {S : H₁ →L[𝕜] H₂} (hS : IsCompactOperator ⇑S) : ∃ (σ : ℕ → ℝ) (u : ℕ → H₁) (v : ℕ → H₂), (∀ (k : ℕ), 0 ≤ σ k) ∧ Antitone σ ∧ OrthonormalOrZero 𝕜 u ∧ OrthonormalOrZero 𝕜 v ∧ (∀ (k : ℕ), σ k ≠ 0 → u k ≠ 0) ∧ (∀ (k : ℕ), σ k ≠ 0 → v k ≠ 0) ∧ Filter.Tendsto σ Filter.atTop (nhds 0) ∧ ∀ (x : H₁), HasSum (fun (k : ℕ) => (↑(σ k) * inner 𝕜 (u k) x) • v k) (S x)

Singular value decomposition / Schmidt representation. Every compact operator between Hilbert spaces has a Schmidt expansion

S x = Σ σₖ ⟨uₖ, x⟩ vₖ,

with orthonormal sequences (uₖ) ⊆ H₁, (vₖ) ⊆ H₂ and singular values σ₀ ≥ σ₁ ≥ ⋯ → 0.

Proof outline (by iterating norm_isSingularValue):

1. Iteration. Set S₀ := S. Given Sₙ (compact), apply IsCompactOperator.norm_isSingularValue to obtain unit vectors uₙ, vₙ with Sₙ uₙ = ‖Sₙ‖ • vₙ and Sₙ* vₙ = ‖Sₙ‖ • uₙ. Set σₙ := ‖Sₙ‖ and Sₙ₊₁ := Sₙ - σₙ • rankOne 𝕜 vₙ uₙ. The rank-one subtrahend is compact (its image is finite-dimensional), and IsCompactOperator is closed under subtraction (IsCompactOperator.sub), so the recursion stays inside the compact-operator class.

2. Orthogonality. By construction Sₙ₊₁ uₙ = 0, so by induction Sₘ uₙ = 0 for all m > n. The variational characterisation of uₘ (the maximiser of ‖Sₘ x‖ on the unit sphere) then forces uₘ ⊥ uₙ: writing uₘ = α uₙ + w with w ⊥ uₙ and using ‖Sₘ uₘ‖² = ‖Sₘ w‖² ≤ ‖Sₘ‖² (1 - |α|²) = σₘ² (1 - |α|²) together with ‖Sₘ uₘ‖ = σₘ gives α = 0 (assuming σₘ > 0). Symmetrically, vₘ ⊥ vₙ (using Sₙ₊₁* vₙ = 0).

3. σₙ → 0. Since S uₙ = σₙ vₙ (using uₙ ⊥ uₘ for m < n) and the vₙ are orthonormal, ‖S uₙ - S uₘ‖² = σₙ² + σₘ². If σₙ stayed ≥ ε > 0, the bounded sequence (uₙ) would map under S to a sequence with no Cauchy subsequence, contradicting compactness of S.

4. Convergence. ‖S - Σₖ<n σₖ • rankOne 𝕜 vₖ uₖ‖ = ‖Sₙ‖ = σₙ → 0, so the Schmidt partial sums converge to S in operator norm; the pointwise HasSum follows.

Eckart–Young: singular values are the approximation numbers

The truncation Sₙ := Σ_{k < n} σₖ ⟨uₖ, ·⟩ vₖ is the best rank-n approximation, with residual ‖S - Sₙ‖ = σₙ. Since the truncation has rank ≤ n, this is ≥ aₙ(S), and minimality gives equality: the k-th singular value equals the k-th approximation number, σₖ = aₖ(S).

theorem SVD.svd_apply_left {𝕜 : Type u} [RCLike 𝕜] {H₁ H₂ : Type u} [NormedAddCommGroup H₁] [InnerProductSpace 𝕜 H₁] [NormedAddCommGroup H₂] [InnerProductSpace 𝕜 H₂] {S : H₁ →L[𝕜] H₂} {σ : ℕ → ℝ} {u : ℕ → H₁} {v : ℕ → H₂} (hu : OrthonormalOrZero 𝕜 u) (htie : ∀ (k : ℕ), σ k ≠ 0 → u k ≠ 0) (hsum : ∀ (x : H₁), HasSum (fun (k : ℕ) => (↑(σ k) * inner 𝕜 (u k) x) • v k) (S x)) (k : ℕ) : S (u k) = ↑(σ k) • v k

From the SVD data, S uₖ = σₖ vₖ (collapse the HasSum at uₖ).

The truncated SVD

Both halves of Eckart–Young below use the truncation Lₘ = ∑_{k<m} σₖ ⟪uₖ, ·⟫ vₖ, and need exactly two facts about it: its rank is at most m, and the residual S − Lₘ has norm at most σₘ. Those are recorded once here.

theorem SVD.svd_sigma_eq_approx {𝕜 : Type u} [RCLike 𝕜] {H₁ H₂ : Type u} [NormedAddCommGroup H₁] [InnerProductSpace 𝕜 H₁] [NormedAddCommGroup H₂] [InnerProductSpace 𝕜 H₂] {S : H₁ →L[𝕜] H₂} {σ : ℕ → ℝ} {u : ℕ → H₁} {v : ℕ → H₂} (hσ0 : ∀ (k : ℕ), 0 ≤ σ k) (hσanti : Antitone σ) (hu : OrthonormalOrZero 𝕜 u) (hv : OrthonormalOrZero 𝕜 v) (hut : ∀ (k : ℕ), σ k ≠ 0 → u k ≠ 0) (hvt : ∀ (k : ℕ), σ k ≠ 0 → v k ≠ 0) (hsum : ∀ (x : H₁), HasSum (fun (k : ℕ) => (↑(σ k) * inner 𝕜 (u k) x) • v k) (S x)) (m : ℕ) : σ m = SNumbers.approximationNumber S m

Eckart–Young. From any SVD of S (OrthonormalOrZero singular vectors with the nonzero-σ tie, and the HasSum Schmidt expansion), the m-th singular value equals the m-th approximation number: σ m = aₘ(S).

theorem SVD.IsCompactOperator.truncation_residual_eq_approxNumber {𝕜 : Type u} [RCLike 𝕜] {H₁ H₂ : Type u} [NormedAddCommGroup H₁] [InnerProductSpace 𝕜 H₁] [CompleteSpace H₁] [NormedAddCommGroup H₂] [InnerProductSpace 𝕜 H₂] [CompleteSpace H₂] {S : H₁ →L[𝕜] H₂} (hS : IsCompactOperator ⇑S) (n : ℕ) : ∃ (L : H₁ →L[𝕜] H₂), L.rank ≤ ↑n ∧ ‖S - L‖ = SNumbers.approximationNumber S n

Eckart–Young. Some rank-n operator L attains the approximation number: ‖S - L‖ = aₙ(S) (the truncated SVD). In particular the infimum defining aₙ(S) is attained on Hilbert spaces.

Diagonal factorisation through ℓ₂ⁿ⁺¹

B ∘ S ∘ A = diag(a₀, …, aₙ), with A : ℓ₂ⁿ⁺¹ → H₁ the isometric inclusion eₖ ↦ uₖ and B : H₂ → ℓ₂ⁿ⁺¹ the contraction y ↦ Σ_{k ≤ n} ⟨vₖ, y⟩ eₖ.

This uses only the top n+1 singular pairs (uₖ, vₖ, σₖ)_{k ≤ n} — a finite slice of the SVD obtained by n+1 iterations of norm_isSingularValue. It needs neither σₖ → 0 nor the HasSum convergence of the full SVD.

theorem SVD.IsCompactOperator.diagonalFactorisation {𝕜 : Type u} [RCLike 𝕜] {H₁ H₂ : Type u} [NormedAddCommGroup H₁] [InnerProductSpace 𝕜 H₁] [CompleteSpace H₁] [NormedAddCommGroup H₂] [InnerProductSpace 𝕜 H₂] [CompleteSpace H₂] {S : H₁ →L[𝕜] H₂} (hS : IsCompactOperator ⇑S) (n : ℕ) : ∃ (A : EuclideanSpace 𝕜 (Fin (n + 1)) →L[𝕜] H₁) (B : H₂ →L[𝕜] EuclideanSpace 𝕜 (Fin (n + 1))), ‖A‖ ≤ 1 ∧ ‖B‖ ≤ 1 ∧ ∀ (k : Fin (n + 1)), B (S (A (EuclideanSpace.single k 1))) = ↑(SNumbers.approximationNumber S ↑k) • EuclideanSpace.single k 1

Diagonal factorisation through ℓ₂ⁿ⁺¹. There is an isometric inclusion A : ℓ₂ⁿ⁺¹ →L[𝕜] H₁ with ‖A‖ ≤ 1 and a contraction B : H₂ →L[𝕜] ℓ₂ⁿ⁺¹ with ‖B‖ ≤ 1 such that on each basis vector,

(B ∘ S ∘ A)(eₖ) = aₖ(S) · eₖ,

i.e. B ∘ S ∘ A = diag(a₀(S), …, aₙ(S)). Built from the top n+1 singular pairs only.

Scalar factorisation (general operators)

Whereas diagonalFactorisation pins the exact values aₖ (so needs S compact, see its note), the scalar factorisation asks only for B ∘ S ∘ A = c • id with c < aₙ(S) strict. It therefore holds for an arbitrary bounded S: for c < aₙ(S) there is an (n+1)-dimensional subspace M ⊆ H₁ on which ‖S x‖ ≥ c ‖x‖ (the variational characterisation of aₙ, valid even when aₙ(S) is not attained — e.g. continuous spectrum); take A to embed ℓ₂ⁿ⁺¹ isometrically onto M, and B to be c times a left inverse of the bounded-below S|_M.

This is the single input the uniqueness theorem for s-numbers (SNumbers.Uniqueness) consumes: chaining (S3) over B ∘ S ∘ A = c • id with the (S5) normalisation sₙ(id) = 1 gives c ≤ sₙ(S) for every c < aₙ(S), hence aₙ(S) ≤ sₙ(S).

theorem SVD.exists_scalar_factorisation {𝕜 : Type u} [RCLike 𝕜] {H₁ H₂ : Type u} [NormedAddCommGroup H₁] [InnerProductSpace 𝕜 H₁] [CompleteSpace H₁] [NormedAddCommGroup H₂] [InnerProductSpace 𝕜 H₂] [CompleteSpace H₂] (S : H₁ →L[𝕜] H₂) (n : ℕ) {c : ℝ} (hc0 : 0 ≤ c) (hc : c < SNumbers.approximationNumber S n) : ∃ (A : EuclideanSpace 𝕜 (Fin (n + 1)) →L[𝕜] H₁) (B : H₂ →L[𝕜] EuclideanSpace 𝕜 (Fin (n + 1))), ‖A‖ ≤ 1 ∧ ‖B‖ ≤ 1 ∧ B ∘SL S ∘SL A = ↑c • ContinuousLinearMap.id 𝕜 (EuclideanSpace 𝕜 (Fin (n + 1)))

Scalar factorisation. For any bounded S : H₁ →L[𝕜] H₂ between Hilbert spaces and any real c with 0 ≤ c < aₙ(S), there are contractions A : ℓ₂ⁿ⁺¹ →L[𝕜] H₁, B : H₂ →L[𝕜] ℓ₂ⁿ⁺¹ with

B ∘ S ∘ A = c • id_{ℓ₂ⁿ⁺¹}.

Proved from SpectralRepresentation.exists_lowerBound_subspace: take an orthonormal basis of the lower-bound subspace M for A, set T := S ∘ A (bounded below by c), and B := c · (T*T)⁻¹ ∘ T* (well-defined since T*T is a unit, via isUnit_of_forall_le_norm_inner_map). No compactness needed.

The leading singular values of a product of Hilbert–Schmidt operators

For a compact operator T = T₂T₁, the sum of the first n+1 singular values is bounded by the product of the Hilbert–Schmidt norms of the two factors,

  (n+1) · aₙ(T) ≤ ∑_{k ≤ n} σₖ(T) ≤ ‖T₁‖_HS · ‖T₂‖_HS ,

the qualitative content of "the nuclear norm is at most the product of the Hilbert–Schmidt norms of the factors" (Pietsch, Eigenvalues and s-numbers, 2.11.23). No Schatten-class theory is needed: the singular values are read off the Schmidt decomposition above, where σₖ = aₖ(T) by Eckart–Young (svd_sigma_eq_approx), and the estimate comes from

  σₖ = re ⟪vₖ, T uₖ⟫ = re ⟪T₂* vₖ, T₁ uₖ⟫ ≤ ‖T₂* vₖ‖ · ‖T₁ uₖ‖

by Cauchy–Schwarz over k ≤ n. The Hilbert–Schmidt property of the factors therefore enters only through the two hypotheses

  ∑ₖ ‖T₁ uₖ‖² ≤ a² and ∑ₖ ‖T₂* vₖ‖² ≤ b²

along arbitrary orthonormal-or-zero families. Those two hypotheses are in turn produced from row data by sum_norm_sq_apply_le_of_rows below, whose input is what BasicResults.LittleGrothendieck supplies for the inclusion ℓ₁ → ℓ_∞ in SNumbers.Examples.IdentityL1Linfty.

theorem SVD.sum_norm_sq_apply_le_of_rows {𝕜 : Type u} [RCLike 𝕜] {H₁ H₂ : Type u} [NormedAddCommGroup H₁] [InnerProductSpace 𝕜 H₁] [NormedAddCommGroup H₂] [InnerProductSpace 𝕜 H₂] {S : H₁ →L[𝕜] H₂} {w : ℕ → H₁} {c : ℝ} (hS : ∀ (x : H₁), ‖S x‖ ^ 2 = ∑' (j : ℕ), ‖inner 𝕜 (w j) x‖ ^ 2) (hc : ∀ (J : Finset ℕ), ∑ j ∈ J, ‖w j‖ ^ 2 ≤ c) {u : ℕ → H₁} (hu : OrthonormalOrZero 𝕜 u) (s : Finset ℕ) : ∑ k ∈ s, ‖S (u k)‖ ^ 2 ≤ c

Bessel plus a row bound. Suppose the operator S is described by a family w of "rows", in the sense that ‖S x‖² = ∑ⱼ |⟪wⱼ, x⟫|², and that the partial sums of ‖wⱼ‖² are bounded by c. Then ∑ₖ ‖S uₖ‖² ≤ c along every orthonormal-or-zero family u.

This is the Hilbert–Schmidt estimate that mul_approximationNumber_le_of_factorization needs for each of its two factors: interchange the two summations (hasSum_sum), apply Bessel's inequality (OrthonormalOrZero.sum_inner_products_le) for each fixed row, and finish with the row bound.

theorem SVD.svd_sigma_le_mul_of_factorization {𝕜 : Type u} [RCLike 𝕜] {H₁ H₂ : Type u} [NormedAddCommGroup H₁] [InnerProductSpace 𝕜 H₁] [NormedAddCommGroup H₂] [InnerProductSpace 𝕜 H₂] [CompleteSpace H₂] {H₃ : Type u} [NormedAddCommGroup H₃] [InnerProductSpace 𝕜 H₃] [CompleteSpace H₃] {T : H₁ →L[𝕜] H₃} {T₁ : H₁ →L[𝕜] H₂} {T₂ : H₂ →L[𝕜] H₃} (hfact : T = T₂ ∘SL T₁) {σ : ℕ → ℝ} {u : ℕ → H₁} {v : ℕ → H₃} (hu : OrthonormalOrZero 𝕜 u) (hv : OrthonormalOrZero 𝕜 v) (hut : ∀ (k : ℕ), σ k ≠ 0 → u k ≠ 0) (hvt : ∀ (k : ℕ), σ k ≠ 0 → v k ≠ 0) (hsum : ∀ (x : H₁), HasSum (fun (k : ℕ) => (↑(σ k) * inner 𝕜 (u k) x) • v k) (T x)) (k : ℕ) : σ k ≤ ‖(ContinuousLinearMap.adjoint T₂) (v k)‖ * ‖T₁ (u k)‖

A single singular value of a factored operator is bounded by the norms of the two factors evaluated at the corresponding singular vectors: σₖ ≤ ‖T₂* vₖ‖ · ‖T₁ uₖ‖. Indeed T uₖ = σₖ vₖ with ‖vₖ‖ = 1 (or σₖ = 0), so σₖ = re ⟪vₖ, T uₖ⟫ = re ⟪T₂* vₖ, T₁ uₖ⟫.

theorem SVD.mul_approximationNumber_le_of_factorization {𝕜 : Type u} [RCLike 𝕜] {H₁ H₂ : Type u} [NormedAddCommGroup H₁] [InnerProductSpace 𝕜 H₁] [CompleteSpace H₁] [NormedAddCommGroup H₂] [InnerProductSpace 𝕜 H₂] [CompleteSpace H₂] {H₃ : Type u} [NormedAddCommGroup H₃] [InnerProductSpace 𝕜 H₃] [CompleteSpace H₃] {T : H₁ →L[𝕜] H₃} (hT : IsCompactOperator ⇑T) {T₁ : H₁ →L[𝕜] H₂} {T₂ : H₂ →L[𝕜] H₃} (hfact : T = T₂ ∘SL T₁) {a b : ℝ} (ha : ∀ (u : ℕ → H₁), OrthonormalOrZero 𝕜 u → ∀ (s : Finset ℕ), ∑ k ∈ s, ‖T₁ (u k)‖ ^ 2 ≤ a ^ 2) (hb : ∀ (v : ℕ → H₃), OrthonormalOrZero 𝕜 v → ∀ (s : Finset ℕ), ∑ k ∈ s, ‖(ContinuousLinearMap.adjoint T₂) (v k)‖ ^ 2 ≤ b ^ 2) (ha0 : 0 ≤ a) (hb0 : 0 ≤ b) (n : ℕ) : (↑n + 1) * SNumbers.approximationNumber T n ≤ b * a

(n+1)·aₙ(T) ≤ ‖T₁‖_HS·‖T₂‖_HS for a factored compact operator.

Let T = T₂T₁ be compact, and suppose that along every orthonormal-or-zero family the two factors satisfy the Hilbert–Schmidt bounds ∑ₖ ‖T₁ uₖ‖² ≤ a² and ∑ₖ ‖T₂* vₖ‖² ≤ b². Then (n+1)·aₙ(T) ≤ ∑_{k≤n} σₖ(T) ≤ b·a for every n.

The first inequality is antitonicity of the singular values, the second is svd_sigma_le_mul_of_factorization followed by Cauchy–Schwarz and the two hypotheses.