Commit 2022-08-19 19:30 0fc54965

View on Github →

feat(linear_algebra/matrix): LDL Decomposition (#15220) Any positive definite matrix S can be decomposed as S = LDLᴴ where L is a lower-triangular matrix and D is a diagonal matrix.

Estimated changes

Modified src/data/matrix/basic.lean

added theorem matrix.mul_mul_apply

Modified src/linear_algebra/matrix/basis.lean

added def basis.invertible_to_matrix

Created src/linear_algebra/matrix/ldl.lean

added theorem LDL.diag_eq_lower_inv_conj

added theorem LDL.lower_conj_diag

added theorem LDL.lower_inv_eq_gram_schmidt_basis

added theorem LDL.lower_inv_orthogonal

added theorem LDL.lower_inv_triangular

Modified src/linear_algebra/matrix/nonsingular_inverse.lean

added theorem matrix.inv_mul_eq_iff_eq_mul_of_invertible

added def matrix.invertible__of_invertible_transpose

added def matrix.invertible_of_invertible_conj_transpose

added theorem matrix.is_unit_of_left_inverse

added theorem matrix.is_unit_of_right_inverse

added theorem matrix.mul_inv_eq_iff_eq_mul_of_invertible

Modified src/linear_algebra/matrix/pos_def.lean

added theorem matrix.pos_def.transpose