# Documentation

Mathlib.LinearAlgebra.Matrix.LDL

# 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} [] {n : Type u_2} [] [IsWellOrder n fun x x_1 => x < x_1] {S : Matrix n n 𝕜} [] (hS : ) :
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.

Instances For
theorem LDL.lowerInv_eq_gramSchmidtBasis {𝕜 : Type u_1} [] {n : Type u_2} [] [IsWellOrder n fun x x_1 => x < x_1] {S : Matrix n n 𝕜} [] (hS : ) :
noncomputable instance LDL.invertibleLowerInv {𝕜 : Type u_1} [] {n : Type u_2} [] [IsWellOrder n fun x x_1 => x < x_1] {S : Matrix n n 𝕜} [] (hS : ) :
theorem LDL.lowerInv_orthogonal {𝕜 : Type u_1} [] {n : Type u_2} [] [IsWellOrder n fun x x_1 => x < x_1] {S : Matrix n n 𝕜} [] (hS : ) {i : n} {j : n} (h₀ : i j) :
inner ((WithLp.equiv 2 (n𝕜)).symm (LDL.lowerInv hS i)) ((WithLp.equiv 2 (n𝕜)).symm (Matrix.mulVec () (LDL.lowerInv hS j))) = 0
noncomputable def LDL.diagEntries {𝕜 : Type u_1} [] {n : Type u_2} [] [IsWellOrder n fun x x_1 => x < x_1] {S : Matrix n n 𝕜} [] (hS : ) :
n𝕜

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

Instances For
noncomputable def LDL.diag {𝕜 : Type u_1} [] {n : Type u_2} [] [IsWellOrder n fun x x_1 => x < x_1] {S : Matrix n n 𝕜} [] (hS : ) :
Matrix n n 𝕜

The diagonal matrix D of the LDL decomposition.

Instances For
theorem LDL.lowerInv_triangular {𝕜 : Type u_1} [] {n : Type u_2} [] [IsWellOrder n fun x x_1 => x < x_1] {S : Matrix n n 𝕜} [] (hS : ) {i : n} {j : n} (hij : i < j) :
LDL.lowerInv hS i j = 0
theorem LDL.diag_eq_lowerInv_conj {𝕜 : Type u_1} [] {n : Type u_2} [] [IsWellOrder n fun x x_1 => x < x_1] {S : Matrix n n 𝕜} [] (hS : ) :
LDL.diag hS = * S *

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} [] {n : Type u_2} [] [IsWellOrder n fun x x_1 => x < x_1] {S : Matrix n n 𝕜} [] (hS : ) :
Matrix n n 𝕜

The lower triangular matrix L of the LDL decomposition.

Instances For
theorem LDL.lower_conj_diag {𝕜 : Type u_1} [] {n : Type u_2} [] [IsWellOrder n fun x x_1 => x < x_1] {S : Matrix n n 𝕜} [] (hS : ) :
* LDL.diag 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.