Polar Decomposition

Statement

Let $A$ be an invertible $n \times n$ complex matrix. Then there exist a unique unitary matrix $U$ and a unique positive definite matrix $P$ such that

The matrix $P = \sqrt{A^* A}$ is the unique positive semidefinite square root of $A^* A$ (which exists because $A^* A$ is Hermitian with non-negative eigenvalues). In the rectangular generalisation ($m \times n$), uniqueness of $U$ is replaced by uniqueness of the restriction to the column space.

Visualization

Take $A = \begin{pmatrix} 3 & 0 \\ 0 & -2 \end{pmatrix}$.

Step 1 — Compute $A^* A$:

Step 2 — Positive definite square root:

Step 3 — Unitary factor:

Verification:

Quantity	Value
$A^* A$	$\text{diag}(9, 4)$
$P = \sqrt{A^* A}$	$\text{diag}(3, 2)$
$U = A P^{-1}$	$\text{diag}(1, -1)$
$U U^*$	$I$ (unitary)
$P^* = P$, $P \ge 0$	positive definite

Proof Sketch

1. Positive semidefiniteness of $A^* A$. For any $v$, $\langle A^* A v, v \rangle = \|Av\|^2 \ge 0$, so $A^* A$ is positive semidefinite. When $A$ is invertible, $\ker A = \{0\}$, so it is positive definite.
2. Square root. By the Spectral TheoremSpectral Theorem$$A = Q \Lambda Q^T \;\text{(real symmetric case)}$$Every real symmetric matrix is orthogonally diagonalizableRead more →, $A^* A = Q D Q^*$ with $D = \text{diag}(\lambda_i)$, $\lambda_i > 0$. Set $P = Q \sqrt{D} Q^*$. Then $P^2 = A^* A$ and $P$ is positive definite.
3. Unitary factor. Set $U = A P^{-1}$. Then $U^* U = (AP^{-1})^* (AP^{-1}) = P^{-1} A^* A P^{-1} = P^{-1} P^2 P^{-1} = I$.
4. Uniqueness. If $A = U_1 P_1 = U_2 P_2$ then $P_1^2 = A^* A = P_2^2$; by uniqueness of the positive definite square root, $P_1 = P_2$, hence $U_1 = U_2$.

Connections

• Spectral TheoremSpectral Theorem$$A = Q \Lambda Q^T \;\text{(real symmetric case)}$$Every real symmetric matrix is orthogonally diagonalizableRead more → — the existence of $P = \sqrt{A^* A}$ rests on spectral diagonalization of the Hermitian matrix $A^* A$
• Determinant MultiplicativityDeterminant Multiplicativity$$\det(AB) = \det(A)\,\det(B)$$The determinant of a product equals the product of determinantsRead more → — $|\det A| = \det P$ since $\det U = 1$ for unitary $U$, and $\det(A^* A) = |\det A|^2$
• Cauchy–Schwarz InequalityCauchy–Schwarz Inequality$$|\langle u, v \rangle| \leq \|u\| \, \|v\|$$The inner product of two vectors is bounded by the product of their normsRead more → — the positive semidefiniteness of $A^* A$ is an instance of the Cauchy–Schwarz inequality applied to the inner product $\langle Av, Av \rangle$

import Mathlib.LinearAlgebra.Matrix.PosDef

/-- The matrix Aᴴ * A is positive semidefinite for any matrix A.
    This is the foundation of polar decomposition: P = sqrt(Aᴴ * A).
    Mathlib's `Matrix.posSemidef_conjTranspose_mul_self` is the direct alias. -/
theorem ata_posSemidef
    {m n : Type*} [Fintype n] [DecidableEq n] [Fintype m]
    (A : Matrix m n ℂ) :
    (Aᴴ * A).PosSemidef :=
  Matrix.posSemidef_conjTranspose_mul_self A