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