The diagonals of the LDL decomposition

Mathlib's LDL decomposition writes a positive-definite matrix S as L * D * Lᴴ with L lower triangular and D diagonal, but records nothing about the individual diagonal entries. This file supplies them: the diagonal of D is positive, and both LDL.lowerInv and LDL.lower carry 1 on the diagonal, so the lower factor of the decomposition is unitriangular.

Main results

• LDL.diagEntries_pos — the diagonal entries of D are positive.
• LDL.lowerInv_apply_diag and LDL.lower_apply_diag — the lower factor of the LDL decomposition and its inverse are unitriangular.

theorem LDL.diagEntries_pos {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [LinearOrder n] [WellFoundedLT n] [LocallyFiniteOrderBot n] [Fintype n] {S : Matrix n n 𝕜} (hS : S.PosDef) (i : n) : 0 < diagEntries hS i

The diagonal entries in Mathlib's LDL decomposition of a positive-definite matrix are positive.

@[simp]

theorem LDL.lowerInv_apply_diag {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [LinearOrder n] [WellFoundedLT n] [LocallyFiniteOrderBot n] [Fintype n] {S : Matrix n n 𝕜} (hS : S.PosDef) (i : n) : lowerInv hS i i = 1

The lower factor in Mathlib's LDL decomposition is unitriangular: its inverse is the Gram-Schmidt matrix, which carries 1 on the diagonal.

@[simp]

theorem LDL.lower_apply_diag {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [LinearOrder n] [WellFoundedLT n] [LocallyFiniteOrderBot n] [Fintype n] {S : Matrix n n 𝕜} (hS : S.PosDef) (i : n) : lower hS i i = 1

The lower factor in Mathlib's LDL decomposition carries 1 on the diagonal, being the inverse of a matrix that does.