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} [RCLike 𝕜] {n : Type u_2} [LinearOrder n] [WellFoundedLT n] [LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [Fintype n] (hS : S.PosDef) : 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} [RCLike 𝕜] {n : Type u_2} [LinearOrder n] [WellFoundedLT n] [LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [Fintype n] (hS : S.PosDef) : LDL.lowerInv hS = ((Pi.basisFun 𝕜 n).toMatrix ⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n))).transpose

noncomputable instance LDL.invertibleLowerInv {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [LinearOrder n] [WellFoundedLT n] [LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [Fintype n] (hS : S.PosDef) : Invertible (LDL.lowerInv hS)

Equations

• LDL.invertibleLowerInv hS = ⋯.mpr inferInstance

theorem LDL.lowerInv_orthogonal {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [LinearOrder n] [WellFoundedLT n] [LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [Fintype n] (hS : S.PosDef) {i j : n} (h₀ : i ≠ j) : inner ((WithLp.equiv 2 (n → 𝕜)).symm (LDL.lowerInv hS i)) ((WithLp.equiv 2 (n → 𝕜)).symm (S.transpose.mulVec (LDL.lowerInv hS j))) = 0

noncomputable def LDL.diagEntries {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [LinearOrder n] [WellFoundedLT n] [LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [Fintype n] (hS : S.PosDef) : n → 𝕜

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

Equations

• LDL.diagEntries hS i = inner ((WithLp.equiv 2 (n → 𝕜)).symm (star (LDL.lowerInv hS i))) ((WithLp.equiv 2 (n → 𝕜)).symm (S.mulVec (star (LDL.lowerInv hS i))))

noncomputable def LDL.diag {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [LinearOrder n] [WellFoundedLT n] [LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [Fintype n] (hS : S.PosDef) : 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} [RCLike 𝕜] {n : Type u_2} [LinearOrder n] [WellFoundedLT n] [LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [Fintype n] (hS : S.PosDef) {i j : n} (hij : i < j) : LDL.lowerInv hS i j = 0

theorem LDL.diag_eq_lowerInv_conj {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [LinearOrder n] [WellFoundedLT n] [LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [Fintype n] (hS : S.PosDef) : LDL.diag hS = LDL.lowerInv hS * S * (LDL.lowerInv hS).conjTranspose

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} [RCLike 𝕜] {n : Type u_2} [LinearOrder n] [WellFoundedLT n] [LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [Fintype n] (hS : S.PosDef) : 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} [RCLike 𝕜] {n : Type u_2} [LinearOrder n] [WellFoundedLT n] [LocallyFiniteOrderBot n] {S : Matrix n n 𝕜} [Fintype n] (hS : S.PosDef) : LDL.lower hS * LDL.diag hS * (LDL.lower hS).conjTranspose = 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.