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} [Fintype n] [CommRing R] [PartialOrder R] [StarOrderedRing R] (M : Matrix n n R) :

Prop

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

source

theorem Matrix.PosDef.isHermitian {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarOrderedRing R] {M : Matrix n n R} (hM : Matrix.PosDef M) :

Matrix.IsHermitian M

source

theorem Matrix.PosDef.re_dotProduct_pos {n : Type u_2} {𝕜 : Type u_4} [Fintype n] [IsROrC 𝕜] {M : Matrix n n 𝕜} (hM : Matrix.PosDef M) {x : n → 𝕜} (hx : x ≠ 0) :

0 < ↑IsROrC.re (Matrix.dotProduct (star x) (Matrix.mulVec M x))

source

def Matrix.PosSemidef {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarOrderedRing R] (M : Matrix n n R) :

Prop

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

Instances For

source

theorem Matrix.PosSemidef.re_dotProduct_nonneg {n : Type u_2} {𝕜 : Type u_4} [Fintype n] [IsROrC 𝕜] {M : Matrix n n 𝕜} (hM : Matrix.PosSemidef M) (x : n → 𝕜) :

0 ≤ ↑IsROrC.re (Matrix.dotProduct (star x) (Matrix.mulVec M x))

source

theorem Matrix.PosDef.posSemidef {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarOrderedRing R] {M : Matrix n n R} (hM : Matrix.PosDef M) :

Matrix.PosSemidef M

source

theorem Matrix.PosSemidef.submatrix {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [CommRing R] [PartialOrder R] [StarOrderedRing R] {M : Matrix n n R} (hM : Matrix.PosSemidef M) (e : m ≃ n) :

Matrix.PosSemidef (Matrix.submatrix M ↑e ↑e)

source

@[simp]

theorem Matrix.posSemidef_submatrix_equiv {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [CommRing R] [PartialOrder R] [StarOrderedRing R] {M : Matrix n n R} (e : m ≃ n) :

Matrix.PosSemidef (Matrix.submatrix M ↑e ↑e) ↔ Matrix.PosSemidef M

source

theorem Matrix.PosDef.transpose {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarOrderedRing R] {M : Matrix n n R} (hM : Matrix.PosDef M) :

Matrix.PosDef (Matrix.transpose M)

source

theorem Matrix.posDef_of_toQuadraticForm' {n : Type u_2} [Fintype n] [DecidableEq n] {M : Matrix n n ℝ} (hM : Matrix.IsSymm M) (hMq : QuadraticForm.PosDef (Matrix.toQuadraticForm' M)) :

Matrix.PosDef M

source

theorem Matrix.posDef_toQuadraticForm' {n : Type u_2} [Fintype n] [DecidableEq n] {M : Matrix n n ℝ} (hM : Matrix.PosDef M) :

QuadraticForm.PosDef (Matrix.toQuadraticForm' M)

source

theorem Matrix.posSemidef_conjTranspose_mul_self {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [CommRing R] [PartialOrder R] [StarOrderedRing R] (A : Matrix m n R) :

Matrix.PosSemidef (Matrix.conjTranspose A * A)

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

source

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

Matrix.PosSemidef (A * Matrix.conjTranspose A)

A matrix multiplied by its conjugate transpose is positive semidefinite

source

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

0 < Matrix.IsHermitian.eigenvalues (_ : Matrix.IsHermitian A) i

The eigenvalues of a positive definite matrix are positive

source

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

0 ≤ Matrix.IsHermitian.eigenvalues (_ : Matrix.IsHermitian A) i

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

source

theorem Matrix.eigenvalues_conjTranspose_mul_self_nonneg {m : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [Fintype m] [Fintype n] [IsROrC 𝕜] (A : Matrix m n 𝕜) [DecidableEq n] (i : n) :

0 ≤ Matrix.IsHermitian.eigenvalues (_ : Matrix.IsHermitian (Matrix.conjTranspose A * A)) i

source

theorem Matrix.eigenvalues_self_mul_conjTranspose_nonneg {m : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [Fintype m] [Fintype n] [IsROrC 𝕜] (A : Matrix m n 𝕜) [DecidableEq m] (i : m) :

0 ≤ Matrix.IsHermitian.eigenvalues (_ : Matrix.IsHermitian (A * Matrix.conjTranspose A)) i

source

theorem Matrix.PosDef.det_pos {n : Type u_2} [Fintype n] {M : Matrix n n ℝ} (hM : Matrix.PosDef M) [DecidableEq n] :

0 < Matrix.det M

source

theorem QuadraticForm.posDef_of_toMatrix' {n : Type u_1} [Fintype n] [DecidableEq n] {Q : QuadraticForm ℝ (n → ℝ)} (hQ : Matrix.PosDef (QuadraticForm.toMatrix' Q)) :

QuadraticForm.PosDef Q

source

theorem QuadraticForm.posDef_toMatrix' {n : Type u_1} [Fintype n] [DecidableEq n] {Q : QuadraticForm ℝ (n → ℝ)} (hQ : QuadraticForm.PosDef Q) :

Matrix.PosDef (QuadraticForm.toMatrix' Q)

source

@[reducible]

noncomputable def Matrix.NormedAddCommGroup.ofMatrix {𝕜 : Type u_1} [IsROrC 𝕜] {n : Type u_2} [Fintype n] {M : Matrix n n 𝕜} (hM : Matrix.PosDef M) :

NormedAddCommGroup (n → 𝕜)

A positive definite matrix M induces a norm ‖x‖ = sqrt (re xᴴMx).

Instances For

source

def Matrix.InnerProductSpace.ofMatrix {𝕜 : Type u_1} [IsROrC 𝕜] {n : Type u_2} [Fintype n] {M : Matrix n n 𝕜} (hM : Matrix.PosDef M) :

InnerProductSpace 𝕜 (n → 𝕜)

A positive definite matrix M induces an inner product ⟪x, y⟫ = xᴴMy.

Instances For