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ᴴMx
is greater than zero for all nonzerox
.Matrix.PosSemidef
: a matrixM : Matrix n n 𝕜
is positive semidefinite if it is Hermitian andxᴴMx
is nonnegative for allx
.
Main results #
Matrix.PosSemidef.fromBlocks₁₁
andMatrix.PosSemidef.fromBlocks₂₂
: If a matrixA
is positive definite, then[A B; Bᴴ D]
is positive semidefinite if and only ifD - Bᴴ A⁻¹ B
is 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.
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.
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.