Commit 2022-10-12 13:05 68ead6e6

View on Github →

feat(linear_algebra/matrix): Schur complement (#15270) If a matrix A is positive definite, then [A B; Bᴴ D] is postive semidefinite if and only if D - Bᴴ A⁻¹ B is postive semidefinite.

Estimated changes

Modified src/algebra/star/pi.lean

added theorem function.star_sum_elim

Modified src/linear_algebra/matrix/hermitian.lean

added theorem matrix.is_hermitian.adjugate

modified theorem matrix.is_hermitian.conj_transpose

added theorem matrix.is_hermitian.inv

modified theorem matrix.is_hermitian.transpose

added theorem matrix.is_hermitian_conj_transpose_iff

added theorem matrix.is_hermitian_conj_transpose_mul_mul

added theorem matrix.is_hermitian_inv

added theorem matrix.is_hermitian_mul_mul_conj_transpose

added theorem matrix.is_hermitian_submatrix_equiv

added theorem matrix.is_hermitian_transpose_iff

Modified src/linear_algebra/matrix/nonsingular_inverse.lean

added theorem matrix.inv_inv_of_invertible

Modified src/linear_algebra/matrix/pos_def.lean

added theorem matrix.pos_def.pos_semidef

added theorem matrix.pos_semidef.submatrix

added def matrix.pos_semidef

added theorem matrix.pos_semidef_submatrix_equiv

Created src/linear_algebra/matrix/schur_complement.lean

added theorem matrix.is_hermitian.from_blocks₁₁

added theorem matrix.is_hermitian.from_blocks₂₂

added theorem matrix.pos_semidef.from_blocks₁₁

added theorem matrix.pos_semidef.from_blocks₂₂

added theorem matrix.schur_complement_eq₁₁

added theorem matrix.schur_complement_eq₂₂