Documentation

DerivedAlgGeo.LinearAlgebra.Matrix.PolarDecomposition

Polar decomposition for invertible matrices #

A = Q * P with Q unitary and P positive definite, over RCLike scalars.

Mathlib has no polar decomposition for matrices at the pinned revision (8a178386) — a search for polarDecomposition across the whole library returns nothing. This file supplies the case this repo needs, in the ForMathlib pattern this repository uses for Mathlib gaps, and is written to be upstreamable rather than to be convenient here.

Why it costs almost nothing now #

The classical proof needs a square root of the positive-definite matrix Aᴴ A, and historically that meant the spectral theorem. It no longer does: Mathlib's continuous functional calculus applies to real matrices once the Loewner order is in scope (open scoped MatrixOrder), so CFC.sqrt is available directly and CFC.sqrt_mul_sqrt_self is the only property needed.

That is the whole trick. P := √(Aᴴ A), Q := A P⁻¹, and

Qᴴ Q = P⁻¹ Aᴴ A P⁻¹ = P⁻¹ (P P) P⁻¹ = 1.

Uniqueness #

Both factors are unique. If A = Q P with Q unitary and P positive definite then Pᴴ Qᴴ Q P = P P, so P is a nonnegative square root of Aᴴ A — and the nonnegative square root is unique (CFC.sqrt_unique), so it is the one. Q = A P⁻¹ then follows.

The positive-definite factor #

source
noncomputable def Matrix.polarFactor {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n 𝕜) :
Matrix n n 𝕜

The positive-definite factor of the polar decomposition, √(Aᴴ A).

Equations
Instances For
    source
    theorem Matrix.polarFactor_posSemidef {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n 𝕜) :
    A.polarFactor.PosSemidef
    source
    theorem Matrix.polarFactor_mul_self {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n 𝕜) :
    A.polarFactor * A.polarFactor = A.conjTranspose * A

    √(Aᴴ A) squares to Aᴴ A. This is the only property of the square root the construction uses.

    source
    theorem Matrix.polarFactor_isHermitian {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n 𝕜) :
    A.polarFactor.IsHermitian
    source
    theorem Matrix.det_polarFactor_ne_zero {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : IsUnit A.det) :
    A.polarFactor.det ≠ 0
    source
    theorem Matrix.isUnit_det_polarFactor {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : IsUnit A.det) :
    IsUnit A.polarFactor.det
    source
    theorem Matrix.polarFactor_posDef {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : IsUnit A.det) :
    A.polarFactor.PosDef

    With A invertible the factor is positive definite, not merely semidefinite.

    The orthogonal factor #

    source
    noncomputable def Matrix.polarUnitary {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n 𝕜) :
    Matrix n n 𝕜

    The unitary factor of the polar decomposition, A · √(Aᴴ A)⁻¹.

    Equations
    Instances For
      source
      theorem Matrix.polarUnitary_mul_polarFactor {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : IsUnit A.det) :
      A.polarUnitary * A.polarFactor = A
      source
      theorem Matrix.polarUnitary_mem_unitaryGroup {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : IsUnit A.det) :
      A.polarUnitary ∈ unitaryGroup n 𝕜
      source
      theorem Matrix.exists_polarDecomposition {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : IsUnit A.det) :
      ∃ Q ∈ unitaryGroup n 𝕜, ∃ (P : Matrix n n 𝕜), P.PosDef ∧ A = Q * P

      Polar decomposition. Every invertible matrix factors as a unitary matrix times a positive-definite one.

      Uniqueness #

      source
      theorem Matrix.eq_polarFactor_of_mul {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A Q P : Matrix n n 𝕜} (hQ : Q ∈ unitaryGroup n 𝕜) (hP : P.PosDef) (hQP : A = Q * P) :
      P = A.polarFactor

      The positive-definite factor is unique.

      source
      theorem Matrix.eq_polarUnitary_of_mul {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : IsUnit A.det) {Q P : Matrix n n 𝕜} (hQ : Q ∈ unitaryGroup n 𝕜) (hP : P.PosDef) (hQP : A = Q * P) :
      Q = A.polarUnitary

      The unitary factor is unique.

      source
      theorem Matrix.existsUnique_polarDecomposition {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : IsUnit A.det) :
      ∃! QP : Matrix n n 𝕜 × Matrix n n 𝕜, QP.1 ∈ unitaryGroup n 𝕜 ∧ QP.2.PosDef ∧ A = QP.1 * QP.2

      Polar decomposition, with uniqueness.