LDL decomposition

This file proves the LDL-decomposition of matrices: Any positive definite matrix S can be decomposed as S = LDLᴴ where L is a lower-triangular matrix and D is a diagonal matrix.

Main definitions

• LDL.lower is the lower triangular matrix L.
• LDL.lowerInv is the inverse of the lower triangular matrix L.
• LDL.diag is the diagonal matrix D.

Main result

• LDL.lower_conj_diag states that any positive definite matrix can be decomposed as LDLᴴ.

TODO

• Prove that LDL.lower is lower triangular from LDL.lowerInv_triangular.

noncomputable def LDL.lowerInv {𝕜 : Type u_1} [IsROrC 𝕜] {n : Type u_2} [LinearOrder n] [IsWellOrder n fun (x x_1 : n) => x < x_1] [LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [Fintype n] (hS : Matrix.PosDef S) : Matrix n n 𝕜

The inverse of the lower triangular matrix L of the LDL-decomposition. It is obtained by applying Gram-Schmidt-Orthogonalization w.r.t. the inner product induced by Sᵀ on the standard basis vectors Pi.basisFun.

Equations

• LDL.lowerInv hS = gramSchmidt 𝕜 ⇑(Pi.basisFun 𝕜 n)

theorem LDL.lowerInv_eq_gramSchmidtBasis {𝕜 : Type u_1} [IsROrC 𝕜] {n : Type u_2} [LinearOrder n] [IsWellOrder n fun (x x_1 : n) => x < x_1] [LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [Fintype n] (hS : Matrix.PosDef S) : LDL.lowerInv hS = Matrix.transpose (Basis.toMatrix (Pi.basisFun 𝕜 n) ⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n)))

noncomputable instance LDL.invertibleLowerInv {𝕜 : Type u_1} [IsROrC 𝕜] {n : Type u_2} [LinearOrder n] [IsWellOrder n fun (x x_1 : n) => x < x_1] [LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [Fintype n] (hS : Matrix.PosDef S) : Invertible (LDL.lowerInv hS)

Equations

• One or more equations did not get rendered due to their size.

theorem LDL.lowerInv_orthogonal {𝕜 : Type u_1} [IsROrC 𝕜] {n : Type u_2} [LinearOrder n] [IsWellOrder n fun (x x_1 : n) => x < x_1] [LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [Fintype n] (hS : Matrix.PosDef S) {i : n} {j : n} (h₀ : i ≠ j) : ⟪(WithLp.equiv 2 (n → 𝕜)).symm (LDL.lowerInv hS i), (WithLp.equiv 2 (n → 𝕜)).symm (Matrix.mulVec (Matrix.transpose S) (LDL.lowerInv hS j))⟫_𝕜 = 0

noncomputable def LDL.diagEntries {𝕜 : Type u_1} [IsROrC 𝕜] {n : Type u_2} [LinearOrder n] [IsWellOrder n fun (x x_1 : n) => x < x_1] [LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [Fintype n] (hS : Matrix.PosDef S) : n → 𝕜

The entries of the diagonal matrix D of the LDL decomposition.

Equations

• LDL.diagEntries hS i = ⟪(WithLp.equiv 2 (n → 𝕜)).symm (star (LDL.lowerInv hS i)), (WithLp.equiv 2 (n → 𝕜)).symm (Matrix.mulVec S (star (LDL.lowerInv hS i)))⟫_𝕜

noncomputable def LDL.diag {𝕜 : Type u_1} [IsROrC 𝕜] {n : Type u_2} [LinearOrder n] [IsWellOrder n fun (x x_1 : n) => x < x_1] [LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [Fintype n] (hS : Matrix.PosDef S) : Matrix n n 𝕜

The diagonal matrix D of the LDL decomposition.

Equations

• LDL.diag hS = Matrix.diagonal (LDL.diagEntries hS)

theorem LDL.lowerInv_triangular {𝕜 : Type u_1} [IsROrC 𝕜] {n : Type u_2} [LinearOrder n] [IsWellOrder n fun (x x_1 : n) => x < x_1] [LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [Fintype n] (hS : Matrix.PosDef S) {i : n} {j : n} (hij : i < j) : LDL.lowerInv hS i j = 0

theorem LDL.diag_eq_lowerInv_conj {𝕜 : Type u_1} [IsROrC 𝕜] {n : Type u_2} [LinearOrder n] [IsWellOrder n fun (x x_1 : n) => x < x_1] [LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [Fintype n] (hS : Matrix.PosDef S) : LDL.diag hS = LDL.lowerInv hS * S * Matrix.conjTranspose (LDL.lowerInv hS)

Inverse statement of LDL decomposition: we can conjugate a positive definite matrix by some lower triangular matrix and get a diagonal matrix.

noncomputable def LDL.lower {𝕜 : Type u_1} [IsROrC 𝕜] {n : Type u_2} [LinearOrder n] [IsWellOrder n fun (x x_1 : n) => x < x_1] [LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [Fintype n] (hS : Matrix.PosDef S) : Matrix n n 𝕜

The lower triangular matrix L of the LDL decomposition.

Equations

• LDL.lower hS = (LDL.lowerInv hS)⁻¹

theorem LDL.lower_conj_diag {𝕜 : Type u_1} [IsROrC 𝕜] {n : Type u_2} [LinearOrder n] [IsWellOrder n fun (x x_1 : n) => x < x_1] [LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [Fintype n] (hS : Matrix.PosDef S) : LDL.lower hS * LDL.diag hS * Matrix.conjTranspose (LDL.lower hS) = S

LDL decomposition: any positive definite matrix S can be decomposed as S = LDLᴴ where L is a lower-triangular matrix and D is a diagonal matrix.