lower — Mathlib

English

For a positive definite matrix S, the LDL decomposition provides a lower triangular L given by L = (LDL.lowerInv hS)^{-1}.

Русский

Для положительно определенной матрицы S нижняя часть LDL-разложения задается как L = (LDL.lowerInv hS)^{-1}.

LaTeX

$$$L = (\text{LDL.lowerInv}(h_S))^{-1}$.$$

Lean4

/-- The lower triangular matrix `L` of the LDL decomposition. -/
noncomputable def lower :=
  (LDL.lowerInv hS)⁻¹

Похожие утверждения