# 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} [] [IsWellOrder n fun (x1 x2 : n) => x1 < x2] {S : Matrix n 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
Instances For
theorem LDL.lowerInv_eq_gramSchmidtBasis {๐ : Type u_1} [RCLike ๐] {n : Type u_2} [] [IsWellOrder n fun (x1 x2 : n) => x1 < x2] {S : Matrix n n ๐} [] (hS : S.PosDef) :
= ((Pi.basisFun ๐ n).toMatrix โ(gramSchmidtBasis (Pi.basisFun ๐ n))).transpose
noncomputable instance LDL.invertibleLowerInv {๐ : Type u_1} [RCLike ๐] {n : Type u_2} [] [IsWellOrder n fun (x1 x2 : n) => x1 < x2] {S : Matrix n n ๐} [] (hS : S.PosDef) :
Equations
• = โฏ.mpr inferInstance
theorem LDL.lowerInv_orthogonal {๐ : Type u_1} [RCLike ๐] {n : Type u_2} [] [IsWellOrder n fun (x1 x2 : n) => x1 < x2] {S : Matrix n n ๐} [] (hS : S.PosDef) {i : n} {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} [] [IsWellOrder n fun (x1 x2 : n) => x1 < x2] {S : Matrix n n ๐} [] (hS : S.PosDef) :
n โ ๐

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

Equations
Instances For
noncomputable def LDL.diag {๐ : Type u_1} [RCLike ๐] {n : Type u_2} [] [IsWellOrder n fun (x1 x2 : n) => x1 < x2] {S : Matrix n n ๐} [] (hS : S.PosDef) :
Matrix n n ๐

The diagonal matrix D of the LDL decomposition.

Equations
Instances For
theorem LDL.lowerInv_triangular {๐ : Type u_1} [RCLike ๐] {n : Type u_2} [] [IsWellOrder n fun (x1 x2 : n) => x1 < x2] {S : Matrix n n ๐} [] (hS : S.PosDef) {i : n} {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} [] [IsWellOrder n fun (x1 x2 : n) => x1 < x2] {S : Matrix n n ๐} [] (hS : S.PosDef) :
LDL.diag 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} [] [IsWellOrder n fun (x1 x2 : n) => x1 < x2] {S : Matrix n n ๐} [] (hS : S.PosDef) :
Matrix n n ๐

The lower triangular matrix L of the LDL decomposition.

Equations
Instances For
theorem LDL.lower_conj_diag {๐ : Type u_1} [RCLike ๐] {n : Type u_2} [] [IsWellOrder n fun (x1 x2 : n) => x1 < x2] {S : Matrix n n ๐} [] (hS : S.PosDef) :
* 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.