Commit 2023-12-18 20:33 448da11d

View on Github →

feat(LinearAlgebra/Matrix/PosDef): unique positive semidef square root (#8809) This PR adds two main results about positive semidefinite matrices:

a positive semidefinite matrix has a unique positive semidefinite square root;
if A is positive semidefinite then x* A x = 0 implies A x = 0 (proof extracted from #8594).

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/Hermitian.lean

added theorem Matrix.isHermitian_diagonal_iff

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

added theorem Matrix.IsHermitian.posSemidef_of_eigenvalues_nonneg

added theorem Matrix.PosSemidef.conjTranspose_mul_mul_same

added def Matrix.PosSemidef.delabSqrt

added theorem Matrix.PosSemidef.dotProduct_mulVec_zero_iff

modified theorem Matrix.PosSemidef.eigenvalues_nonneg

added theorem Matrix.PosSemidef.eq_of_sq_eq_sq

added theorem Matrix.PosSemidef.eq_sqrt_of_sq_eq

added theorem Matrix.PosSemidef.isHermitian

added theorem Matrix.PosSemidef.mul_mul_conjTranspose_same

added theorem Matrix.PosSemidef.posSemidef_sqrt

modified theorem Matrix.PosSemidef.re_dotProduct_nonneg

added theorem Matrix.PosSemidef.sq_sqrt

added theorem Matrix.PosSemidef.sqrt_mul_self

added theorem Matrix.PosSemidef.sqrt_sq

modified theorem Matrix.PosSemidef.submatrix

added theorem Matrix.PosSemidef.toLinearMap₂'_zero_iff

added theorem Matrix.PosSemidef.transpose

modified theorem Matrix.posSemidef_conjTranspose_mul_self

added theorem Matrix.posSemidef_diagonal_iff

added theorem Matrix.posSemidef_iff_eq_transpose_mul_self

modified theorem Matrix.posSemidef_self_mul_conjTranspose

Modified Mathlib/LinearAlgebra/Matrix/Spectrum.lean

added theorem Matrix.IsHermitian.exists_eigenvector_of_ne_zero

added theorem Matrix.IsHermitian.mulVec_eigenvectorBasis