# mathlib3documentation

linear_algebra.matrix.ldl

# LDL decomposition #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves the LDL-decomposition of matricies: 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.lower_inv is the inverse of the lower triangular matrix L.
• LDL.diag is the diagonal matrix D.

## Main result #

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

## TODO #

• Prove that LDL.lower is lower triangular from LDL.lower_inv_triangular.
noncomputable def LDL.lower_inv {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [linear_order n] {S : n 𝕜} [fintype n] (hS : S.pos_def) :
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.basis_fun.

Equations
Instances for LDL.lower_inv
theorem LDL.lower_inv_eq_gram_schmidt_basis {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [linear_order n] {S : n 𝕜} [fintype n] (hS : S.pos_def) :
@[protected, instance]
noncomputable def LDL.invertible_lower_inv {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [linear_order n] {S : n 𝕜} [fintype n] (hS : S.pos_def) :
Equations
theorem LDL.lower_inv_orthogonal {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [linear_order n] {S : n 𝕜} [fintype n] (hS : S.pos_def) {i j : n} (h₀ : i j) :
has_inner.inner (((pi_Lp.equiv 2 (λ (ᾰ : n), 𝕜)).symm) i)) (((pi_Lp.equiv 2 (λ (i : n), 𝕜)).symm) (S.transpose.mul_vec j))) = 0
noncomputable def LDL.diag_entries {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [linear_order n] {S : n 𝕜} [fintype n] (hS : S.pos_def) :
n 𝕜

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

Equations
noncomputable def LDL.diag {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [linear_order n] {S : n 𝕜} [fintype n] (hS : S.pos_def) :
n 𝕜

The diagonal matrix D of the LDL decomposition.

Equations
theorem LDL.lower_inv_triangular {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [linear_order n] {S : n 𝕜} [fintype n] (hS : S.pos_def) {i j : n} (hij : i < j) :
i j = 0
theorem LDL.diag_eq_lower_inv_conj {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [linear_order n] {S : n 𝕜} [fintype n] (hS : S.pos_def) :

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} [is_R_or_C 𝕜] {n : Type u_2} [linear_order n] {S : n 𝕜} [fintype n] (hS : S.pos_def) :
n 𝕜

The lower triangular matrix L of the LDL decomposition.

Equations
theorem LDL.lower_conj_diag {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [linear_order n] {S : n 𝕜} [fintype n] (hS : S.pos_def) :

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.