# 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 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.

##Β Main results

• Matrix.posSemidef_iff_eq_transpose_mul_self : a matrix M : Matrix n n π is positive semidefinite iff it has the form Bα΄΄ * B for some B.
• Matrix.PosSemidef.sqrt : the unique positive semidefinite square root of a positive semidefinite matrix. (See Matrix.PosSemidef.eq_sqrt_of_sq_eq for the proof of uniqueness.)

## Positive semidefinite matrices #

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α΄΄ * M * x is nonnegative for all x.

Equations
Instances For
theorem Matrix.posSemidef_diagonal_iff {n : Type u_2} {R : Type u_3} [] [] [] [] [] [] {d : n β R} :
().PosSemidef β β (i : n), 0 β€ d i

A diagonal matrix is positive semidefinite iff its diagonal entries are nonnegative.

theorem Matrix.PosSemidef.isHermitian {n : Type u_2} {R : Type u_3} [] [] [] [] [] {M : Matrix n n R} (hM : M.PosSemidef) :
M.IsHermitian
theorem Matrix.PosSemidef.re_dotProduct_nonneg {n : Type u_2} {π : Type u_4} [] [RCLike π] {M : Matrix n n π} (hM : M.PosSemidef) (x : n β π) :
0 β€ RCLike.re (Matrix.dotProduct (star x) (M.mulVec x))
theorem Matrix.PosSemidef.conjTranspose_mul_mul_same {n : Type u_2} {R : Type u_3} [] [] [] [] [] {A : Matrix n n R} (hA : A.PosSemidef) {m : Type u_5} [] (B : Matrix n m R) :
(B.conjTranspose * A * B).PosSemidef
theorem Matrix.PosSemidef.mul_mul_conjTranspose_same {n : Type u_2} {R : Type u_3} [] [] [] [] [] {A : Matrix n n R} (hA : A.PosSemidef) {m : Type u_5} [] (B : Matrix m n R) :
(B * A * B.conjTranspose).PosSemidef
theorem Matrix.PosSemidef.submatrix {m : Type u_1} {n : Type u_2} {R : Type u_3} [] [] [] [] [] [] {M : Matrix n n R} (hM : M.PosSemidef) (e : m β n) :
(M.submatrix e e).PosSemidef
theorem Matrix.PosSemidef.transpose {n : Type u_2} {R : Type u_3} [] [] [] [] [] {M : Matrix n n R} (hM : M.PosSemidef) :
M.transpose.PosSemidef
theorem Matrix.PosSemidef.conjTranspose {n : Type u_2} {R : Type u_3} [] [] [] [] [] {M : Matrix n n R} (hM : M.PosSemidef) :
M.conjTranspose.PosSemidef
theorem Matrix.PosSemidef.zero {n : Type u_2} {R : Type u_3} [] [] [] [] [] :
theorem Matrix.PosSemidef.one {n : Type u_2} {R : Type u_3} [] [] [] [] [] [] :
theorem Matrix.PosSemidef.pow {n : Type u_2} {R : Type u_3} [] [] [] [] [] [] {M : Matrix n n R} (hM : M.PosSemidef) (k : β) :
(M ^ k).PosSemidef
theorem Matrix.PosSemidef.inv {n : Type u_2} {R : Type u_3} [] [] [] [] [] [] {M : Matrix n n R} (hM : M.PosSemidef) :
.PosSemidef
theorem Matrix.PosSemidef.zpow {n : Type u_2} {R : Type u_3} [] [] [] [] [] [] {M : Matrix n n R} (hM : M.PosSemidef) (z : β€) :
(M ^ z).PosSemidef
theorem Matrix.PosSemidef.eigenvalues_nonneg {n : Type u_2} {π : Type u_4} [] [RCLike π] [] {A : Matrix n n π} (hA : A.PosSemidef) (i : n) :
0 β€ β―.eigenvalues i

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

noncomputable def Matrix.PosSemidef.sqrt {n : Type u_2} {π : Type u_4} [] [RCLike π] [] {A : Matrix n n π} (hA : A.PosSemidef) :
Matrix n n π

The positive semidefinite square root of a positive semidefinite matrix

Equations
Instances For

Custom elaborator to produce output like (_ : PosSemidef A).sqrt in the goal view.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Matrix.PosSemidef.posSemidef_sqrt {n : Type u_2} {π : Type u_4} [] [RCLike π] [] {A : Matrix n n π} (hA : A.PosSemidef) :
hA.sqrt.PosSemidef
@[simp]
theorem Matrix.PosSemidef.sq_sqrt {n : Type u_2} {π : Type u_4} [] [RCLike π] [] {A : Matrix n n π} (hA : A.PosSemidef) :
hA.sqrt ^ 2 = A
@[simp]
theorem Matrix.PosSemidef.sqrt_mul_self {n : Type u_2} {π : Type u_4} [] [RCLike π] [] {A : Matrix n n π} (hA : A.PosSemidef) :
hA.sqrt * hA.sqrt = A
theorem Matrix.PosSemidef.eq_of_sq_eq_sq {n : Type u_2} {π : Type u_4} [] [RCLike π] [] {A : Matrix n n π} (hA : A.PosSemidef) {B : Matrix n n π} (hB : B.PosSemidef) (hAB : A ^ 2 = B ^ 2) :
A = B
theorem Matrix.PosSemidef.sqrt_sq {n : Type u_2} {π : Type u_4} [] [RCLike π] [] {A : Matrix n n π} (hA : A.PosSemidef) :
(β― : (A ^ 2).PosSemidef).sqrt = A
theorem Matrix.PosSemidef.eq_sqrt_of_sq_eq {n : Type u_2} {π : Type u_4} [] [RCLike π] [] {A : Matrix n n π} (hA : A.PosSemidef) {B : Matrix n n π} (hB : B.PosSemidef) (hAB : A ^ 2 = B) :
A = hB.sqrt
@[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) :
(M.submatrix βe βe).PosSemidef β M.PosSemidef
theorem Matrix.posSemidef_conjTranspose_mul_self {m : Type u_1} {n : Type u_2} {R : Type u_3} [] [] [] [] [] [] (A : Matrix m n R) :
(A.conjTranspose * A).PosSemidef

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 * A.conjTranspose).PosSemidef

A matrix multiplied by its conjugate transpose is positive semidefinite

theorem Matrix.eigenvalues_conjTranspose_mul_self_nonneg {m : Type u_1} {n : Type u_2} {π : Type u_4} [] [] [RCLike π] (A : Matrix m n π) [] (i : n) :
0 β€ β―.eigenvalues i
theorem Matrix.eigenvalues_self_mul_conjTranspose_nonneg {m : Type u_1} {n : Type u_2} {π : Type u_4} [] [] [RCLike π] (A : Matrix m n π) [] (i : m) :
0 β€ β―.eigenvalues i
theorem Matrix.posSemidef_iff_eq_transpose_mul_self {n : Type u_2} {π : Type u_4} [] [RCLike π] {A : Matrix n n π} :
A.PosSemidef β β (B : Matrix n n π), A = B.conjTranspose * B

A matrix is positive semidefinite if and only if it has the form Bα΄΄ * B for some B.

theorem Matrix.IsHermitian.posSemidef_of_eigenvalues_nonneg {n : Type u_2} {π : Type u_4} [] [RCLike π] [] {A : Matrix n n π} (hA : A.IsHermitian) (h : β (i : n), 0 β€ hA.eigenvalues i) :
A.PosSemidef
theorem Matrix.PosSemidef.dotProduct_mulVec_zero_iff {n : Type u_2} {π : Type u_4} [] [RCLike π] {A : Matrix n n π} (hA : A.PosSemidef) (x : n β π) :
Matrix.dotProduct (star x) (A.mulVec x) = 0 β A.mulVec x = 0

For A positive semidefinite, we have xβ A x = 0 iff A x = 0.

theorem Matrix.PosSemidef.toLinearMapβ'_zero_iff {n : Type u_2} {π : Type u_4} [] [RCLike π] [] {A : Matrix n n π} (hA : A.PosSemidef) (x : n β π) :
((Matrix.toLinearMapβ' A) (star x)) x = 0 β (Matrix.toLin' A) x = 0

For A positive semidefinite, we have xβ A x = 0 iff A x = 0 (linear maps version).

## Positive definite matrices #

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.

Equations
Instances For
theorem Matrix.PosDef.isHermitian {n : Type u_2} {R : Type u_3} [] [] [] [] [] {M : Matrix n n R} (hM : M.PosDef) :
M.IsHermitian
theorem Matrix.PosDef.re_dotProduct_pos {n : Type u_2} {π : Type u_4} [] [RCLike π] {M : Matrix n n π} (hM : M.PosDef) {x : n β π} (hx : x β  0) :
0 < RCLike.re (Matrix.dotProduct (star x) (M.mulVec x))
theorem Matrix.PosDef.posSemidef {n : Type u_2} {R : Type u_3} [] [] [] [] [] {M : Matrix n n R} (hM : M.PosDef) :
M.PosSemidef
theorem Matrix.PosDef.transpose {n : Type u_2} {R : Type u_3} [] [] [] [] [] {M : Matrix n n R} (hM : M.PosDef) :
M.transpose.PosDef
theorem Matrix.PosDef.of_toQuadraticForm' {n : Type u_2} [] [] {M : } (hM : M.IsSymm) (hMq : M.toQuadraticForm'.PosDef) :
M.PosDef
theorem Matrix.PosDef.toQuadraticForm' {n : Type u_2} [] [] {M : } (hM : M.PosDef) :
theorem Matrix.PosDef.eigenvalues_pos {n : Type u_2} {π : Type u_4} [] [RCLike π] [] {A : Matrix n n π} (hA : A.PosDef) (i : n) :
0 < β―.eigenvalues i

The eigenvalues of a positive definite matrix are positive

theorem Matrix.PosDef.det_pos {n : Type u_2} {π : Type u_4} [] [RCLike π] [] {M : Matrix n n π} (hM : M.PosDef) :
0 < M.det
theorem QuadraticForm.posDef_of_toMatrix' {n : Type u_1} [] [] {Q : QuadraticForm β (n β β)} (hQ : Q.toMatrix'.PosDef) :
Q.PosDef
theorem QuadraticForm.posDef_toMatrix' {n : Type u_1} [] [] {Q : QuadraticForm β (n β β)} (hQ : Q.PosDef) :
Q.toMatrix'.PosDef
@[reducible, inline]
noncomputable abbrev Matrix.NormedAddCommGroup.ofMatrix {π : Type u_1} [RCLike π] {n : Type u_2} [] {M : Matrix n n π} (hM : M.PosDef) :

A positive definite matrix M induces a norm βxβ = sqrt (re xα΄΄Mx).

Equations
A positive definite matrix M induces an inner product βͺx, yβ« = xα΄΄My.