Singular value decomposition

TheoremUnitary reduction of a complex matrix to rectangular diagonal form#✓fully proved

Every rectangular complex matrix becomes rectangular diagonal after a unitary change of basis on the right, with a further unitary change of basis on the codomain (S. Axler, Linear Algebra Done Right, 4th ed., Section 7E).

theorem exists_unitaryGroup_mul_eq_rectangularDiagonal
    (m n : ℕ) (A : Matrix (Fin m) (Fin n) ℂ) :
    ∃ (U : Matrix.unitaryGroup (Fin m) ℂ) (V : Matrix.unitaryGroup (Fin n) ℂ)
        (σ : Fin n → ℝ),
      (∀ j, 0 ≤ σ j) ∧ Antitone σ ∧ (∀ j, m ≤ j.val → σ j = 0) ∧
      A * (V : Matrix (Fin n) (Fin n) ℂ) =
        (U : Matrix (Fin m) (Fin m) ℂ) *
          Matrix.of (fun i j => if i.val = j.val then (σ j : ℂ) else 0)
Used by 1
Used byComplex SVD with nonincreasing singular values

TheoremComplex SVD with nonincreasing singular values#✓fully proved

This is the rectangular complex SVD with singular values in nonincreasing order.

Proof: Multiply the rectangular-diagonal factorization on the right by Vᴴ.

theorem exists_unitaryGroup_rectangularDiagonal_antitone
    (m n : ℕ) (A : Matrix (Fin m) (Fin n) ℂ) :
    ∃ (U : Matrix.unitaryGroup (Fin m) ℂ) (V : Matrix.unitaryGroup (Fin n) ℂ)
        (σ : Fin n → ℝ),
      (∀ j, 0 ≤ σ j) ∧ Antitone σ ∧ (∀ j, m ≤ j.val → σ j = 0) ∧
      A = (U : Matrix (Fin m) (Fin m) ℂ) *
        Matrix.of (fun i j => if i.val = j.val then (σ j : ℂ) else 0) *
          star (V : Matrix (Fin n) (Fin n) ℂ)
Uses 1 · Used by 1
Proof usesUnitary reduction of a complex matrix to rectangular diagonal form
Used bySingular value decomposition of a complex matrix

TheoremSquared Frobenius norm as the sum of squared singular values#✓fully proved

Frobenius-norm identity for an SVD: the sum of the squared singular values is the sum of the squared norms of the entries.

theorem sum_sq_singularValues_eq_sum_sq_norm_of_svd {m n : ℕ}
    (A : Matrix (Fin m) (Fin n) ℂ) {U : Matrix (Fin m) (Fin m) ℂ}
    {V : Matrix (Fin n) (Fin n) ℂ}
    (hU : U ∈ Matrix.unitaryGroup (Fin m) ℂ) (hV : V ∈ Matrix.unitaryGroup (Fin n) ℂ)
    {σ : Fin n → ℝ} (hσ : ∀ j, m ≤ j.val → σ j = 0)
    (hA : A = U * Matrix.of (fun i j => if i.val = j.val then (σ j : ℂ) else 0) * star V) :
    ∑ j, σ j ^ 2 = ∑ i, ∑ j, ‖A i j‖ ^ 2

TheoremSingular value decomposition of a complex matrix#✓fully proved

Rectangular complex singular value decomposition: every complex m × n matrix factors as U * Σ * Vᴴ with U and V unitary and Σ rectangular diagonal with nonnegative entries; the singular values beyond the first min m n (indices j with m ≤ j.val) are zero.

Proof: Apply the spectral theorem to AᴴA, normalize the images of the eigenvectors with positive eigenvalues, and extend them to an orthonormal basis of the codomain, as in the proof of S. Axler, Linear Algebra Done Right, 4th ed., 7.70, and the matrix form that follows it (Section 7E).

theorem complex_singular_value_decomposition (m n : ℕ) (A : Matrix (Fin m) (Fin n) ℂ) :
    ∃ (U : Matrix (Fin m) (Fin m) ℂ) (V : Matrix (Fin n) (Fin n) ℂ) (σ : Fin n → ℝ),
      (∀ j, 0 ≤ σ j) ∧ (∀ j, m ≤ j.val → σ j = 0) ∧
      U ∈ Matrix.unitaryGroup (Fin m) ℂ ∧ V ∈ Matrix.unitaryGroup (Fin n) ℂ ∧
      A = U * Matrix.of (fun i j => if i.val = j.val then (σ j : ℂ) else 0) *
        star V
Sources
  • S. Axler, Linear Algebra Done Right, 4th ed., Section 7E; G. H. Golub and C. F. Van Loan, Matrix Computations, 4th ed., Johns Hopkins University Press (2013), Theorem 2.4.1.
Uses 1
Proof usesComplex SVD with nonincreasing singular values

TheoremSingular value decomposition of a complex square matrix#✓fully proved

Let \(A\) be a square complex matrix whose rows and columns are indexed by a finite type \(n\). Then there are unitary matrices \(U\) and \(V\) and nonnegative real numbers \(\sigma_i\) for \(i \in n\) such that, writing \(D\) for the diagonal matrix with diagonal entries \(\sigma_i\) and \(V^*\) for the conjugate transpose of \(V\), we have \(A = U D V^*\).

theorem exists_unitaryGroup_diagonal_nonneg (A : Matrix n n ℂ) :
    ∃ (U V : Matrix.unitaryGroup n ℂ) (σ : n → ℝ), (∀ i, 0 ≤ σ i) ∧
      A = (U : Matrix n n ℂ) * diagonal (fun i => (σ i : ℂ)) * star (V : Matrix n n ℂ)
Sources
  • R. A. Horn and C. R. Johnson, Matrix Analysis, 2nd ed., Cambridge University Press (2013).
Used by 1
Used byPolar decomposition of a complex square matrix

TheoremOrthogonal reduction of a real matrix to rectangular diagonal form#✓fully proved

Let \(A\) be a real \(m \times n\) matrix. Then there are orthogonal matrices \(U\) of size \(m \times m\) and \(V\) of size \(n \times n\) and real numbers \(\sigma_1 \ge \sigma_2 \ge \dots \ge \sigma_n \ge 0\) with \(\sigma_j = 0\) for every \(j > m\), such that \(AV = U\Sigma\), where \(\Sigma\) is the \(m \times n\) matrix with \(\Sigma_{jj} = \sigma_j\) for \(j \le \min(m, n)\) and all other entries zero.

theorem exists_orthogonalGroup_mul_eq_rectangularDiagonal
    (m n : ℕ) (A : Matrix (Fin m) (Fin n) ℝ) :
    ∃ (U : Matrix.orthogonalGroup (Fin m) ℝ) (V : Matrix.orthogonalGroup (Fin n) ℝ)
        (σ : Fin n → ℝ),
      (∀ j, 0 ≤ σ j) ∧ Antitone σ ∧ (∀ j, m ≤ j.val → σ j = 0) ∧
      A * (V : Matrix (Fin n) (Fin n) ℝ) =
        (U : Matrix (Fin m) (Fin m) ℝ) *
          Matrix.of (fun i j => if i.val = j.val then σ j else 0)
Sources
  • S. Axler, Linear Algebra Done Right, 4th ed., Section 7E.
Used by 1
Used byReal singular value decomposition with nonincreasing singular values

TheoremReal singular value decomposition with nonincreasing singular values#✓fully proved

Let \(A\) be a real \(m \times n\) matrix. Then there are orthogonal matrices \(U\) of size \(m \times m\) and \(V\) of size \(n \times n\) and real numbers \(\sigma_1 \ge \sigma_2 \ge \dots \ge \sigma_n \ge 0\) with \(\sigma_j = 0\) for every \(j > m\), such that \(A = U \Sigma V^{\mathsf{T}}\), where \(\Sigma\) is the \(m \times n\) matrix with \(\Sigma_{jj} = \sigma_j\) for \(j \le \min(m, n)\) and all other entries zero.

Proof: multiply the factorization \(AV = U\Sigma\) on the right by \(V^{\mathsf{T}}\).

theorem exists_orthogonalGroup_rectangularDiagonal_antitone
    (m n : ℕ) (A : Matrix (Fin m) (Fin n) ℝ) :
    ∃ (U : Matrix.orthogonalGroup (Fin m) ℝ) (V : Matrix.orthogonalGroup (Fin n) ℝ)
        (σ : Fin n → ℝ),
      (∀ j, 0 ≤ σ j) ∧ Antitone σ ∧ (∀ j, m ≤ j.val → σ j = 0) ∧
      A = (U : Matrix (Fin m) (Fin m) ℝ) *
        Matrix.of (fun i j => if i.val = j.val then σ j else 0) *
          Matrix.transpose (V : Matrix (Fin n) (Fin n) ℝ)
Uses 1 · Used by 1
Proof usesOrthogonal reduction of a real matrix to rectangular diagonal form
Used byReal singular value decomposition

TheoremReal singular value decomposition#✓fully proved

Let \(A\) be a real \(m \times n\) matrix. Then there are orthogonal matrices \(U\) of size \(m \times m\) and \(V\) of size \(n \times n\) and real numbers \(\sigma_1, \dots, \sigma_n \ge 0\) with \(\sigma_j = 0\) for every \(j > m\), such that \(A = U \Sigma V^{\mathsf{T}}\), where \(\Sigma\) is the \(m \times n\) matrix with \(\Sigma_{jj} = \sigma_j\) for \(j \le \min(m, n)\) and all other entries zero.

Proof: apply the spectral theorem to \(A^{\mathsf{T}} A\), normalize the images under \(A\) of the eigenvectors with positive eigenvalues, and extend them to an orthonormal basis of \(\mathbb{R}^m\), as in the proof of S. Axler, Linear Algebra Done Right, 4th ed., 7.70, and the matrix form that follows it (Section 7E).

theorem real_singular_value_decomposition (m n : ℕ) (A : Matrix (Fin m) (Fin n) ℝ) :
    ∃ (U : Matrix (Fin m) (Fin m) ℝ) (V : Matrix (Fin n) (Fin n) ℝ) (σ : Fin n → ℝ),
      (∀ j, 0 ≤ σ j) ∧ (∀ j, m ≤ j.val → σ j = 0) ∧
      U ∈ Matrix.orthogonalGroup (Fin m) ℝ ∧ V ∈ Matrix.orthogonalGroup (Fin n) ℝ ∧
      A = U * Matrix.of (fun i j => if i.val = j.val then σ j else 0) *
        Matrix.transpose V
Sources
  • G. H. Golub and C. F. Van Loan, Matrix Computations, 4th ed., Johns Hopkins University Press (2013), Theorem 2.4.1.
Uses 1
Proof usesReal singular value decomposition with nonincreasing singular values
8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.