Positive Definite Matrices #
This file defines positive (semi)definite matrices and connects the notion to positive definiteness
of quadratic forms. Most results require 𝕜 = ℝ or ℂ.
Main definitions #
Matrix.PosDef: a matrixM : Matrix n n 𝕜is positive definite if it is Hermitian andxᴴMxis greater than zero for all nonzerox.Matrix.PosSemidef: a matrixM : Matrix n n 𝕜is positive semidefinite if it is Hermitian andxᴴMxis nonnegative for allx.
Main results #
Matrix.PosSemidef.fromBlocks₁₁andMatrix.PosSemidef.fromBlocks₂₂: If a matrixAis positive definite, then[A B; Bᴴ D]is positive semidefinite if and only ifD - Bᴴ A⁻¹ Bis positive semidefinite.
Positive semidefinite matrices #
A matrix M : Matrix n n R is positive semidefinite if it is Hermitian and xᴴ * M * x is
nonnegative for all x.
Equations
- M.PosSemidef = (M.IsHermitian ∧ ∀ (x : n → R), 0 ≤ star x ⬝ᵥ M.mulVec x)
Instances For
A diagonal matrix is positive semidefinite iff its diagonal entries are nonnegative.
The eigenvalues of a positive semi-definite matrix are non-negative
The conjugate transpose of a matrix multiplied by the matrix is positive semidefinite
A matrix multiplied by its conjugate transpose is positive semidefinite
A Hermitian matrix is positive semi-definite if and only if its eigenvalues are non-negative.
Alias of the reverse direction of Matrix.IsHermitian.posSemidef_iff_eigenvalues_nonneg.
A Hermitian matrix is positive semi-definite if and only if its eigenvalues are non-negative.
For an invertible matrix U, star U * x * U is positive semi-definite iff x is.
This works on any ⋆-ring with a partial order.
See IsUnit.conjugate_nonneg_iff' for a similar statement for star-ordered rings.
For an invertible matrix U, U * x * star U is positive semi-definite iff x is.
This works on any ⋆-ring with a partial order.
See IsUnit.conjugate_nonneg_iff for a similar statement for star-ordered rings.
The matrix vecMulVec a (star a) is always positive semi-definite.
The matrix vecMulVec (star a) a is always postive semi-definite.
Positive definite matrices #
A matrix M : Matrix n n R is positive definite if it is Hermitian
and xᴴMx is greater than zero for all nonzero x.
Instances For
The eigenvalues of a positive definite matrix are positive
A Hermitian matrix is positive-definite if and only if its eigenvalues are positive.
For an invertible matrix U, star U * x * U is positive definite iff x is.
This works on any ⋆-ring with a partial order.
See IsUnit.isStrictlyPositive_conjugate_iff' for a similar statement for star-ordered rings.
For matrices, positive definiteness is equivalent to strict positivity when the underlying field is
ℝ or ℂ (see Matrix.isStrictlyPositive_iff_posDef).
For an invertible matrix U, U * x * star U is positive definite iff x is.
This works on any ⋆-ring with a partial order.
See IsUnit.isStrictlyPositive_conjugate_iff for a similar statement for star-ordered rings.
For matrices, positive definiteness is equivalent to strict positivity when the underlying field is
ℝ or ℂ (see Matrix.isStrictlyPositive_iff_posDef).
A positive definite matrix M induces a norm ‖x‖ = sqrt (re xᴴMx).
Instances For
A positive definite matrix M induces an inner product ⟪x, y⟫ = xᴴMy.
Equations
- One or more equations did not get rendered due to their size.