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} [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ᴴ * M * x is nonnegative for all x.

Equations

• Matrix.PosSemidef M = (Matrix.IsHermitian M ∧ ∀ (x : n → R), 0 ≤ Matrix.dotProduct (star x) (Matrix.mulVec M x))

theorem Matrix.posSemidef_diagonal_iff {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarOrderedRing R] [DecidableEq n] {d : n → R} : Matrix.PosSemidef (Matrix.diagonal d) ↔ ∀ (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} [Fintype n] [CommRing R] [PartialOrder R] [StarOrderedRing R] {M : Matrix n n R} (hM : Matrix.PosSemidef M) : Matrix.IsHermitian M

theorem Matrix.PosSemidef.re_dotProduct_nonneg {n : Type u_2} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] {M : Matrix n n 𝕜} (hM : Matrix.PosSemidef M) (x : n → 𝕜) : 0 ≤ RCLike.re (Matrix.dotProduct (star x) (Matrix.mulVec M x))

theorem Matrix.PosSemidef.conjTranspose_mul_mul_same {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarOrderedRing R] {A : Matrix n n R} (hA : Matrix.PosSemidef A) {m : Type u_5} [Fintype m] (B : Matrix n m R) : Matrix.PosSemidef (Matrix.conjTranspose B * A * B)

theorem Matrix.PosSemidef.mul_mul_conjTranspose_same {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarOrderedRing R] {A : Matrix n n R} (hA : Matrix.PosSemidef A) {m : Type u_5} [Fintype m] (B : Matrix m n R) : Matrix.PosSemidef (B * A * Matrix.conjTranspose B)

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)

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

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

theorem Matrix.PosSemidef.zero {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarOrderedRing R] : Matrix.PosSemidef 0

theorem Matrix.PosSemidef.one {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarOrderedRing R] [DecidableEq n] : Matrix.PosSemidef 1

theorem Matrix.PosSemidef.pow {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarOrderedRing R] [DecidableEq n] {M : Matrix n n R} (hM : Matrix.PosSemidef M) (k : ℕ) : Matrix.PosSemidef (M ^ k)

theorem Matrix.PosSemidef.inv {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarOrderedRing R] [DecidableEq n] {M : Matrix n n R} (hM : Matrix.PosSemidef M) : Matrix.PosSemidef M⁻¹

theorem Matrix.PosSemidef.zpow {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarOrderedRing R] [DecidableEq n] {M : Matrix n n R} (hM : Matrix.PosSemidef M) (z : ℤ) : Matrix.PosSemidef (M ^ z)

theorem Matrix.PosSemidef.eigenvalues_nonneg {n : Type u_2} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.PosSemidef A) (i : n) : 0 ≤ Matrix.IsHermitian.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} [Fintype n] [RCLike 𝕜] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.PosSemidef A) : Matrix n n 𝕜

The positive semidefinite square root of a positive semidefinite matrix

Equations

• One or more equations did not get rendered due to their size.

def Matrix.PosSemidef.delabSqrt : Lean.PrettyPrinter.Delaborator.Delab

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.

theorem Matrix.PosSemidef.posSemidef_sqrt {n : Type u_2} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.PosSemidef A) : Matrix.PosSemidef hA.sqrt

@[simp]

theorem Matrix.PosSemidef.sq_sqrt {n : Type u_2} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.PosSemidef A) : hA.sqrt ^ 2 = A

@[simp]

theorem Matrix.PosSemidef.sqrt_mul_self {n : Type u_2} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.PosSemidef A) : hA.sqrt * hA.sqrt = A

theorem Matrix.PosSemidef.eq_of_sq_eq_sq {n : Type u_2} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.PosSemidef A) {B : Matrix n n 𝕜} (hB : Matrix.PosSemidef B) (hAB : A ^ 2 = B ^ 2) : A = B

theorem Matrix.PosSemidef.sqrt_sq {n : Type u_2} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.PosSemidef A) : (⋯ : Matrix.PosSemidef (A ^ 2)).sqrt = A

theorem Matrix.PosSemidef.eq_sqrt_of_sq_eq {n : Type u_2} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.PosSemidef A) {B : Matrix n n 𝕜} (hB : Matrix.PosSemidef B) (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} [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

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

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

theorem Matrix.eigenvalues_conjTranspose_mul_self_nonneg {m : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [Fintype m] [Fintype n] [RCLike 𝕜] (A : Matrix m n 𝕜) [DecidableEq n] (i : n) : 0 ≤ Matrix.IsHermitian.eigenvalues ⋯ i

theorem Matrix.eigenvalues_self_mul_conjTranspose_nonneg {m : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [Fintype m] [Fintype n] [RCLike 𝕜] (A : Matrix m n 𝕜) [DecidableEq m] (i : m) : 0 ≤ Matrix.IsHermitian.eigenvalues ⋯ i

theorem Matrix.posSemidef_iff_eq_transpose_mul_self {n : Type u_2} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] {A : Matrix n n 𝕜} : Matrix.PosSemidef A ↔ ∃ (B : Matrix n n 𝕜), A = Matrix.conjTranspose B * 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} [Fintype n] [RCLike 𝕜] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.IsHermitian A) (h : ∀ (i : n), 0 ≤ Matrix.IsHermitian.eigenvalues hA i) : Matrix.PosSemidef A

theorem Matrix.PosSemidef.dotProduct_mulVec_zero_iff {n : Type u_2} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : Matrix.PosSemidef A) (x : n → 𝕜) : Matrix.dotProduct (star x) (Matrix.mulVec A x) = 0 ↔ Matrix.mulVec A 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} [Fintype n] [RCLike 𝕜] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.PosSemidef A) (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} [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.

Equations

• Matrix.PosDef M = (Matrix.IsHermitian M ∧ ∀ (x : n → R), x ≠ 0 → 0 < Matrix.dotProduct (star x) (Matrix.mulVec M x))

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

theorem Matrix.PosDef.re_dotProduct_pos {n : Type u_2} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] {M : Matrix n n 𝕜} (hM : Matrix.PosDef M) {x : n → 𝕜} (hx : x ≠ 0) : 0 < RCLike.re (Matrix.dotProduct (star x) (Matrix.mulVec M x))

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

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)

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

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)

theorem Matrix.PosDef.eigenvalues_pos {n : Type u_2} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.PosDef A) (i : n) : 0 < Matrix.IsHermitian.eigenvalues ⋯ i

The eigenvalues of a positive definite matrix are positive

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

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

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

@[reducible]

noncomputable def Matrix.NormedAddCommGroup.ofMatrix {𝕜 : Type u_1} [RCLike 𝕜] {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).

Equations

• Matrix.NormedAddCommGroup.ofMatrix hM = InnerProductSpace.Core.toNormedAddCommGroup

def Matrix.InnerProductSpace.ofMatrix {𝕜 : Type u_1} [RCLike 𝕜] {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.

Equations

• One or more equations did not get rendered due to their size.