The Cholesky equivalence

This file proves uniqueness of positive-diagonal lower-triangular Gram factors. Together with the Cholesky construction, this packages Cholesky factorization and reconstruction as an equivalence between positive-definite symmetric matrices and positive-diagonal lower-triangular matrices.

Main results

• TauCeti.eq_cholesky_of_mul_transpose_self_eq identifies any positive-diagonal lower-triangular Gram factor with the Cholesky factor.
• TauCeti.cholesky_choleskyReconstruction is the inverse identity from factors to matrices.
• TauCeti.choleskyEquiv is the resulting equivalence.

References

• R. A. Horn and C. R. Johnson, Matrix Analysis, second edition, Cambridge University Press, 2013, Section 7.2.

theorem TauCeti.eq_cholesky_of_mul_transpose_self_eq {p : ℕ} (A : PosDefMatrix p) (L : PosDiagLowerTriangular p) (hL : ↑L * (↑L).transpose = ↑↑A) : L = cholesky A

A positive-diagonal lower-triangular square root of a positive-definite matrix is its Cholesky factor.

@[simp]

theorem TauCeti.cholesky_choleskyReconstruction {p : ℕ} (L : PosDiagLowerTriangular p) : cholesky (choleskyReconstruction L) = L

Taking the Cholesky factor after reconstructing a matrix from a positive-diagonal lower-triangular factor returns that factor.

noncomputable def TauCeti.choleskyEquiv {p : ℕ} : PosDefMatrix p ≃ PosDiagLowerTriangular p

Cholesky factorization is an equivalence between positive-definite symmetric matrices and positive-diagonal lower-triangular matrices.

Equations

• TauCeti.choleskyEquiv = { toFun := TauCeti.cholesky, invFun := TauCeti.choleskyReconstruction, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.choleskyEquiv_apply {p : ℕ} (A : PosDefMatrix p) : choleskyEquiv A = cholesky A

The forward map of choleskyEquiv is cholesky.

@[simp]

theorem TauCeti.choleskyEquiv_symm_apply {p : ℕ} (L : PosDiagLowerTriangular p) : choleskyEquiv.symm L = choleskyReconstruction L

The inverse map of choleskyEquiv is choleskyReconstruction.