# Documentation

Mathlib.LinearAlgebra.Matrix.PosDef

# Positive Definite Matrices #

This file defines positive (semi)definite matrices and connects the notion to positive definiteness of quadratic forms.

## Main definition #

• Matrix.PosDef : a matrix M : Matrix n n 𝕜 is positive definite if it is hermitian and xᴴMx is greater than zero for all nonzero x.
• Matrix.PosSemidef : a matrix M : Matrix n n 𝕜 is positive semidefinite if it is hermitian and xᴴMx is nonnegative for all x.
def Matrix.PosDef {n : Type u_2} {R : Type u_3} [] [] [] [] (M : Matrix n n R) :

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
theorem Matrix.PosDef.isHermitian {n : Type u_2} {R : Type u_3} [] [] [] [] {M : Matrix n n R} (hM : ) :
theorem Matrix.PosDef.re_dotProduct_pos {n : Type u_2} {𝕜 : Type u_4} [] [] {M : Matrix n n 𝕜} (hM : ) {x : n𝕜} (hx : x 0) :
0 < IsROrC.re (Matrix.dotProduct (star x) ())
def Matrix.PosSemidef {n : Type u_2} {R : Type u_3} [] [] [] [] (M : Matrix n n R) :

A matrix M : Matrix n n R is positive semidefinite if it is hermitian and xᴴMx is nonnegative for all x.

Instances For
theorem Matrix.PosSemidef.re_dotProduct_nonneg {n : Type u_2} {𝕜 : Type u_4} [] [] {M : Matrix n n 𝕜} (hM : ) (x : n𝕜) :
0 IsROrC.re (Matrix.dotProduct (star x) ())
theorem Matrix.PosDef.posSemidef {n : Type u_2} {R : Type u_3} [] [] [] [] {M : Matrix n n R} (hM : ) :
theorem Matrix.PosSemidef.submatrix {m : Type u_1} {n : Type u_2} {R : Type u_3} [] [] [] [] [] {M : Matrix n n R} (hM : ) (e : m n) :
@[simp]
theorem Matrix.posSemidef_submatrix_equiv {m : Type u_1} {n : Type u_2} {R : Type u_3} [] [] [] [] [] {M : Matrix n n R} (e : m n) :
theorem Matrix.PosDef.transpose {n : Type u_2} {R : Type u_3} [] [] [] [] {M : Matrix n n R} (hM : ) :
theorem Matrix.posDef_of_toQuadraticForm' {n : Type u_2} [] [] {M : Matrix n n } (hM : ) (hMq : ) :
theorem Matrix.posDef_toQuadraticForm' {n : Type u_2} [] [] {M : Matrix n n } (hM : ) :
theorem Matrix.posSemidef_conjTranspose_mul_self {m : Type u_1} {n : Type u_2} {R : Type u_3} [] [] [] [] [] (A : Matrix m n R) :

The conjugate transpose of a matrix mulitplied by the matrix is positive semidefinite

theorem Matrix.posSemidef_self_mul_conjTranspose {m : Type u_1} {n : Type u_2} {R : Type u_3} [] [] [] [] [] (A : Matrix m n R) :

A matrix multiplied by its conjugate transpose is positive semidefinite

theorem Matrix.PosDef.eigenvalues_pos {n : Type u_2} {𝕜 : Type u_4} [] [] [] {A : Matrix n n 𝕜} (hA : ) (i : n) :

The eigenvalues of a positive definite matrix are positive

theorem Matrix.PosSemidef.eigenvalues_nonneg {n : Type u_2} {𝕜 : Type u_4} [] [] [] {A : Matrix n n 𝕜} (hA : ) (i : n) :

The eigenvalues of a positive semi-definite matrix are non-negative

theorem Matrix.eigenvalues_conjTranspose_mul_self_nonneg {m : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [] [] [] (A : Matrix m n 𝕜) [] (i : n) :
0
theorem Matrix.eigenvalues_self_mul_conjTranspose_nonneg {m : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [] [] [] (A : Matrix m n 𝕜) [] (i : m) :
0
theorem Matrix.PosDef.det_pos {n : Type u_2} [] {M : Matrix n n } (hM : ) [] :
0 <
theorem QuadraticForm.posDef_of_toMatrix' {n : Type u_1} [] [] {Q : QuadraticForm (n)} (hQ : ) :
theorem QuadraticForm.posDef_toMatrix' {n : Type u_1} [] [] {Q : QuadraticForm (n)} (hQ : ) :
@[reducible]
noncomputable def Matrix.NormedAddCommGroup.ofMatrix {𝕜 : Type u_1} [] {n : Type u_2} [] {M : Matrix n n 𝕜} (hM : ) :
A positive definite matrix M induces a norm ‖x‖ = sqrt (re xᴴMx).
A positive definite matrix M induces an inner product ⟪x, y⟫ = xᴴMy.