Polar decomposition

TheoremPolar decomposition of a complex square matrix#✓fully proved

Let \(A\) be a square complex matrix indexed by a finite type, and let \(A^*\) be its conjugate transpose. Then there are a unitary matrix \(U\) and a positive semidefinite matrix \(P\) such that \(P^2 = A^* A\) and \(A = UP\).

theorem exists_unitaryGroup_posSemidef (A : Matrix n n ℂ) :
    ∃ (U : Matrix.unitaryGroup n ℂ) (P : Matrix n n ℂ),
      P.PosSemidef ∧ P * P = Aᴴ * A ∧ A = (U : Matrix n n ℂ) * P

Sources

R. A. Horn and C. R. Johnson, Matrix Analysis, 2nd ed., Cambridge University Press (2013).

Uses 1

Proof usesSingular value decomposition of a complex square matrix

TheoremUniqueness of the polar decomposition of an invertible matrix#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \(A\) be a square matrix over \(\mathbb{K}\), indexed by a finite type, with \(\det A \neq 0\). Then there are a unitary matrix \(U\) and a positive-definite matrix \(P\) with \(A = UP\), and they are unique: if \(U'\) is unitary, \(P'\) is positive definite and \(A = U'P'\), then \(U' = U\) and \(P' = P\).

theorem exists_unique_unitaryGroup_posDef_of_isUnit_det [DecidableEq n]
    (A : Matrix n n 𝕜) (hA : IsUnit A.det) :
    ∃ (U : Matrix.unitaryGroup n 𝕜) (P : Matrix n n 𝕜),
      P.PosDef ∧ A = (U : Matrix n n 𝕜) * P ∧
        ∀ (U' : Matrix.unitaryGroup n 𝕜) (P' : Matrix n n 𝕜),
          P'.PosDef → A = (U' : Matrix n n 𝕜) * P' → U' = U ∧ P' = P

Used by 2

Used byPolar decomposition of invertible complex matrices · Polar decomposition of invertible real matrices

TheoremPolar decomposition of invertible real matrices#✓fully proved

Let \(A\) be a real square matrix with rows and columns indexed by a finite set, and suppose \(\det A \ne 0\). Then there are an orthogonal matrix \(O\) and a positive-definite symmetric matrix \(S\) with \(A = OS\), and they are unique: if \(O'\) is orthogonal, \(S'\) is positive-definite symmetric and \(A = O'S'\), then \(O' = O\) and \(S' = S\).

Proof: take \(S\) to be the positive-definite square root of \(A^{\mathsf{T}} A\) and \(O = AS^{-1}\), the construction in Wikipedia, "Polar decomposition".

theorem polar_decomposition_gl_real (A : Matrix n n ℝ) (hA : IsUnit A.det) :
    ∃ O S : Matrix n n ℝ,
      O ∈ Matrix.orthogonalGroup n ℝ ∧ S.PosDef ∧ A = O * S ∧
        ∀ O' S' : Matrix n n ℝ,
          O' ∈ Matrix.orthogonalGroup n ℝ → S'.PosDef → A = O' * S' → O' = O ∧ S' = S

Sources

R. A. Horn and C. R. Johnson, Matrix Analysis, 2nd ed., Cambridge University Press (2013), Theorem 7.3.1.

Uses 1

Proof usesUniqueness of the polar decomposition of an invertible matrix

TheoremPolar decomposition of invertible complex matrices#✓fully proved

Let \(A\) be a complex square matrix with rows and columns indexed by a finite set, and suppose \(\det A \ne 0\). Then there are a unitary matrix \(U\) and a positive-definite Hermitian matrix \(P\) with \(A = UP\), and they are unique: if \(U'\) is unitary, \(P'\) is positive-definite Hermitian and \(A = U'P'\), then \(U' = U\) and \(P' = P\).

Proof: take \(P\) to be the positive-definite square root of \(A^* A\) and \(U = AP^{-1}\), the construction in Wikipedia, "Polar decomposition".

theorem polar_decomposition_gl_complex (A : Matrix n n ℂ) (hA : IsUnit A.det) :
    ∃ U P : Matrix n n ℂ,
      U ∈ Matrix.unitaryGroup n ℂ ∧ P.PosDef ∧ A = U * P ∧
        ∀ U' P' : Matrix n n ℂ,
          U' ∈ Matrix.unitaryGroup n ℂ → P'.PosDef → A = U' * P' → U' = U ∧ P' = P

Sources

R. A. Horn and C. R. Johnson, Matrix Analysis, 2nd ed., Cambridge University Press (2013), Theorem 7.3.1.

Uses 1

Proof usesUniqueness of the polar decomposition of an invertible matrix

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.