English
Any positive definite matrix S can be written as S = L D L^{*} where L is lower triangular and D is diagonal.
Русский
Любая положительно определенная матрица S имеет представление S = L D L^{*}, где L – нижняя треугольная, а D – диагональная.
LaTeX
$$$S = L D L^{*} \quad (L \text{ lower triangular}, D \text{ diagonal})$$$
Lean4
/-- **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. -/
theorem lower_conj_diag : LDL.lower hS * LDL.diag hS * (LDL.lower hS)ᴴ = S :=
by
rw [LDL.lower, conjTranspose_nonsing_inv, Matrix.mul_assoc,
Matrix.inv_mul_eq_iff_eq_mul_of_invertible (LDL.lowerInv hS), Matrix.mul_inv_eq_iff_eq_mul_of_invertible]
exact LDL.diag_eq_lowerInv_conj hS
