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.

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) : lowerInv hS = ((Pi.basisFun 𝕜 n).toMatrix ⇑(InnerProductSpace.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 (lowerInv hS)

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.toLp 2 (lowerInv hS i)) (WithLp.toLp 2 (S.transpose.mulVec (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.

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.

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) : 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) : diag hS = lowerInv hS * S * (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.

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) : lower hS * diag hS * (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.