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 #

def Matrix.PosDef {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarOrderedRing R] (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.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))
    def Matrix.PosSemidef {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarOrderedRing R] (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} [Fintype n] [IsROrC 𝕜] {M : Matrix n n 𝕜} (hM : Matrix.PosSemidef M) (x : n𝕜) :
      0 IsROrC.re (Matrix.dotProduct (star x) (Matrix.mulVec M x))
      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) :
      @[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) :

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

      A matrix multiplied by its conjugate transpose is positive semidefinite

      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) :

      The eigenvalues of a positive definite matrix are positive

      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) :

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

      theorem Matrix.PosDef.det_pos {n : Type u_2} [Fintype n] {M : Matrix n n } (hM : Matrix.PosDef M) [DecidableEq n] :
      @[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
        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