English
Let S be a positive definite matrix. If L and D denote the LDL components, then the diagonal part D is obtained by conjugating S with L from the left (equivalently, D = L^{-1} S (L^{-1})^{*}), and S can be reconstructed as S = L D L^{*} with L lower triangular and D diagonal.
Русский
Пусть S – положительно определенная матрица. Обозначим через L и D соответствующие компоненты LDL-разложения: диагональная часть S получается как D = L^{-1} S (L^{-1})^{*}, и при этом S восстанавливается как S = L D L^{*}, где L – нижнетреугольная, а D – диагональная.
LaTeX
$$$\text{Let } S \text{ be positive definite. Let } L = \text{lower}(S) \text{ and } D = \text{diag}(S). \\ D = L^{-1} S (L^{-1})^{*}, \quad S = L D L^{*}. $$$
Lean4
/-- Inverse statement of **LDL decomposition**: we can conjugate a positive definite matrix
by some lower triangular matrix and get a diagonal matrix. -/
theorem diag_eq_lowerInv_conj : LDL.diag hS = LDL.lowerInv hS * S * (LDL.lowerInv hS)ᴴ :=
by
ext i j
by_cases hij : i = j
· simp only [diag, diagEntries, EuclideanSpace.inner_toLp_toLp, star_star, hij, diagonal_apply_eq, Matrix.mul_assoc,
dotProduct_comm]
rfl
· simp only [LDL.diag, hij, diagonal_apply_ne, Ne, not_false_iff, mul_mul_apply]
rw [conjTranspose, transpose_map, transpose_transpose, dotProduct_mulVec,
(LDL.lowerInv_orthogonal hS fun h : j = i => hij h.symm).symm, ← inner_conj_symm, mulVec_transpose,
EuclideanSpace.inner_toLp_toLp, ← RCLike.star_def, ← star_dotProduct_star, star_star]
rfl
