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. Most results require 𝕜 = ℝ or .

Main definitions #

Main results #

Positive semidefinite matrices #

def Matrix.PosSemidef {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] (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 {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] {d : nR} (h : 0 d) :
    theorem Matrix.posSemidef_diagonal_iff {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] {d : nR} :
    (diagonal d).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} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {M : Matrix n n R} (hM : M.PosSemidef) :
    theorem Matrix.PosSemidef.re_dotProduct_nonneg {n : Type u_2} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] {M : Matrix n n 𝕜} (hM : M.PosSemidef) (x : n𝕜) :
    theorem Matrix.PosSemidef.conjTranspose_mul_mul_same {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {A : Matrix n n R} (hA : A.PosSemidef) {m : Type u_6} [Fintype m] (B : Matrix n m R) :
    theorem Matrix.PosSemidef.mul_mul_conjTranspose_same {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {A : Matrix n n R} (hA : A.PosSemidef) {m : Type u_6} [Fintype m] (B : Matrix m n R) :
    theorem Matrix.PosSemidef.submatrix {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {M : Matrix n n R} (hM : M.PosSemidef) (e : mn) :
    theorem Matrix.PosSemidef.transpose {n : Type u_2} {R' : Type u_4} [Fintype n] [CommRing R'] [PartialOrder R'] [StarRing R'] {M : Matrix n n R'} (hM : M.PosSemidef) :
    @[simp]
    theorem Matrix.posSemidef_transpose_iff {n : Type u_2} {R' : Type u_4} [Fintype n] [CommRing R'] [PartialOrder R'] [StarRing R'] {M : Matrix n n R'} :
    theorem Matrix.PosSemidef.conjTranspose {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {M : Matrix n n R} (hM : M.PosSemidef) :
    theorem Matrix.PosSemidef.zero {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] :
    theorem Matrix.PosSemidef.natCast {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] (d : ) :
    (↑d).PosSemidef
    theorem Matrix.PosSemidef.intCast {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] (d : ) (hd : 0 d) :
    (↑d).PosSemidef
    @[simp]
    theorem Matrix.posSemidef_intCast_iff {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [Nonempty n] [Nontrivial R] (d : ) :
    (↑d).PosSemidef 0 d
    theorem Matrix.PosSemidef.pow {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] {M : Matrix n n R} (hM : M.PosSemidef) (k : ) :
    theorem Matrix.PosSemidef.inv {n : Type u_2} {R' : Type u_4} [Fintype n] [CommRing R'] [PartialOrder R'] [StarRing R'] [DecidableEq n] {M : Matrix n n R'} (hM : M.PosSemidef) :
    theorem Matrix.PosSemidef.zpow {n : Type u_2} {R' : Type u_4} [Fintype n] [CommRing R'] [PartialOrder R'] [StarRing R'] [StarOrderedRing R'] [DecidableEq n] {M : Matrix n n R'} (hM : M.PosSemidef) (z : ) :
    theorem Matrix.PosSemidef.add {m : Type u_1} {R : Type u_3} [Fintype m] [Ring R] [PartialOrder R] [StarRing R] [AddLeftMono R] {A B : Matrix m m R} (hA : A.PosSemidef) (hB : B.PosSemidef) :
    theorem Matrix.PosSemidef.smul {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {α : Type u_6} [CommSemiring α] [PartialOrder α] [StarRing α] [StarOrderedRing α] [Algebra α R] [StarModule α R] [PosSMulMono α R] {x : Matrix n n R} (hx : x.PosSemidef) {a : α} (ha : 0 a) :
    theorem Matrix.PosSemidef.eigenvalues_nonneg {n : Type u_2} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.PosSemidef) (i : n) :

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

    theorem Matrix.PosSemidef.trace_nonneg {n : Type u_2} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : A.PosSemidef) :
    theorem Matrix.PosSemidef.det_nonneg {n : Type u_2} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.PosSemidef) :
    0 M.det
    @[simp]
    theorem Matrix.posSemidef_submatrix_equiv {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {M : Matrix n n R} (e : m n) :
    theorem Matrix.posSemidef_conjTranspose_mul_self {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] (A : Matrix m n R) :

    The conjugate transpose of a matrix multiplied 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] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] (A : Matrix m n R) :

    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_5} [Fintype m] [Fintype n] [RCLike 𝕜] (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_5} [Fintype m] [Fintype n] [RCLike 𝕜] (A : Matrix m n 𝕜) [DecidableEq m] (i : m) :
    theorem Matrix.IsHermitian.posSemidef_iff_eigenvalues_nonneg {n : Type u_2} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) :

    A Hermitian matrix is positive semi-definite if and only if its eigenvalues are non-negative.

    @[deprecated Matrix.IsHermitian.posSemidef_iff_eigenvalues_nonneg (since := "2025-08-17")]
    theorem Matrix.IsHermitian.posSemidef_of_eigenvalues_nonneg {n : Type u_2} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) :

    Alias of the reverse direction of Matrix.IsHermitian.posSemidef_iff_eigenvalues_nonneg.


    A Hermitian matrix is positive semi-definite if and only if its eigenvalues are non-negative.

    theorem Matrix.PosSemidef.trace_eq_zero_iff {n : Type u_2} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : A.PosSemidef) :
    A.trace = 0 A = 0
    theorem Matrix.posSemidef_vecMulVec_self_star {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] (a : nR) :

    The matrix vecMulVec a (star a) is always positive semi-definite.

    theorem Matrix.posSemidef_vecMulVec_star_self {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] (a : nR) :

    The matrix vecMulVec (star a) a is always postive semi-definite.

    Positive definite matrices #

    def Matrix.PosDef {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing 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.

    Equations
    Instances For
      theorem Matrix.PosDef.isHermitian {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {M : Matrix n n R} (hM : M.PosDef) :
      theorem Matrix.PosDef.re_dotProduct_pos {n : Type u_2} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] {M : Matrix n n 𝕜} (hM : M.PosDef) {x : n𝕜} (hx : x 0) :
      theorem Matrix.PosDef.posSemidef {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {M : Matrix n n R} (hM : M.PosDef) :
      theorem Matrix.PosDef.transpose {n : Type u_2} {R' : Type u_4} [Fintype n] [CommRing R'] [PartialOrder R'] [StarRing R'] {M : Matrix n n R'} (hM : M.PosDef) :
      @[simp]
      theorem Matrix.PosDef.transpose_iff {n : Type u_2} {R' : Type u_4} [Fintype n] [CommRing R'] [PartialOrder R'] [StarRing R'] {M : Matrix n n R'} :
      theorem Matrix.PosDef.diagonal {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] {d : nR} (h : ∀ (i : n), 0 < d i) :
      @[simp]
      theorem Matrix.posDef_diagonal_iff {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] [Nontrivial R] {d : nR} :
      (diagonal d).PosDef ∀ (i : n), 0 < d i
      theorem Matrix.PosDef.natCast {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] (d : ) (hd : d 0) :
      (↑d).PosDef
      @[simp]
      theorem Matrix.posDef_natCast_iff {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] [Nonempty n] [Nontrivial R] {d : } :
      (↑d).PosDef 0 < d
      theorem Matrix.PosDef.intCast {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] (d : ) (hd : 0 < d) :
      (↑d).PosDef
      @[simp]
      theorem Matrix.posDef_intCast_iff {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] [Nonempty n] [Nontrivial R] {d : } :
      (↑d).PosDef 0 < d
      theorem Matrix.PosDef.add_posSemidef {m : Type u_1} {R : Type u_3} [Fintype m] [Ring R] [PartialOrder R] [StarRing R] [AddLeftMono R] {A B : Matrix m m R} (hA : A.PosDef) (hB : B.PosSemidef) :
      (A + B).PosDef
      theorem Matrix.PosDef.posSemidef_add {m : Type u_1} {R : Type u_3} [Fintype m] [Ring R] [PartialOrder R] [StarRing R] [AddLeftMono R] {A B : Matrix m m R} (hA : A.PosSemidef) (hB : B.PosDef) :
      (A + B).PosDef
      theorem Matrix.PosDef.add {m : Type u_1} {R : Type u_3} [Fintype m] [Ring R] [PartialOrder R] [StarRing R] [AddLeftMono R] {A B : Matrix m m R} (hA : A.PosDef) (hB : B.PosDef) :
      (A + B).PosDef
      theorem Matrix.PosDef.smul {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {α : Type u_6} [CommSemiring α] [PartialOrder α] [StarRing α] [StarOrderedRing α] [Algebra α R] [StarModule α R] [PosSMulStrictMono α R] {x : Matrix n n R} (hx : x.PosDef) {a : α} (ha : 0 < a) :
      (a x).PosDef
      theorem Matrix.PosDef.conjTranspose_mul_mul_same {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {A : Matrix n n R} {B : Matrix n m R} (hA : A.PosDef) (hB : Function.Injective B.mulVec) :
      theorem Matrix.PosDef.mul_mul_conjTranspose_same {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {A : Matrix n n R} {B : Matrix m n R} (hA : A.PosDef) (hB : Function.Injective fun (v : mR) => vecMul v B) :
      theorem Matrix.PosDef.mul_conjTranspose_self {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [NoZeroDivisors R] (A : Matrix m n R) (hA : Function.Injective fun (v : mR) => vecMul v A) :
      theorem Matrix.PosDef.conjTranspose {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {M : Matrix n n R} (hM : M.PosDef) :
      @[simp]
      theorem Matrix.posDef_conjTranspose_iff {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {M : Matrix n n R} :
      theorem Matrix.PosDef.eigenvalues_pos {n : Type u_2} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.PosDef) (i : n) :
      0 < .eigenvalues i

      The eigenvalues of a positive definite matrix are positive

      theorem Matrix.IsHermitian.posDef_iff_eigenvalues_pos {n : Type u_2} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) :
      A.PosDef ∀ (i : n), 0 < hA.eigenvalues i

      A Hermitian matrix is positive-definite if and only if its eigenvalues are positive.

      theorem Matrix.PosDef.trace_pos {n : Type u_2} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] [Nonempty n] {A : Matrix n n 𝕜} (hA : A.PosDef) :
      0 < A.trace
      theorem Matrix.PosDef.det_pos {n : Type u_2} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.PosDef) :
      0 < M.det
      theorem Matrix.PosDef.isUnit {n : Type u_2} [Fintype n] {K : Type u_6} [Field K] [PartialOrder K] [StarRing K] [DecidableEq n] {M : Matrix n n K} (hM : M.PosDef) :
      theorem Matrix.PosDef.inv {n : Type u_2} [Fintype n] {K : Type u_6} [Field K] [PartialOrder K] [StarRing K] [DecidableEq n] {M : Matrix n n K} (hM : M.PosDef) :
      @[simp]
      theorem Matrix.posDef_inv_iff {n : Type u_2} [Fintype n] {K : Type u_6} [Field K] [PartialOrder K] [StarRing K] [DecidableEq n] {M : Matrix n n K} :
      theorem Matrix.PosDef.fromBlocks₁₁ {m : Type u_1} {n : Type u_2} {R' : Type u_4} [Fintype m] [Fintype n] [CommRing R'] [PartialOrder R'] [StarRing R'] [StarOrderedRing R'] [DecidableEq m] {A : Matrix m m R'} (B : Matrix m n R') (D : Matrix n n R') (hA : A.PosDef) [Invertible A] :
      theorem Matrix.PosDef.fromBlocks₂₂ {m : Type u_1} {n : Type u_2} {R' : Type u_4} [Fintype m] [Fintype n] [CommRing R'] [PartialOrder R'] [StarRing R'] [StarOrderedRing R'] [DecidableEq n] (A : Matrix m m R') (B : Matrix m n R') {D : Matrix n n R'} (hD : D.PosDef) [Invertible D] :
      @[reducible, inline]
      noncomputable abbrev Matrix.NormedAddCommGroup.ofMatrix {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {M : Matrix n n 𝕜} (hM : M.PosDef) :
      NormedAddCommGroup (n𝕜)

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

      Equations
      Instances For
        def Matrix.InnerProductSpace.ofMatrix {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {M : Matrix n n 𝕜} (hM : M.PosDef) :
        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.
        Instances For