HepLean 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 #

source
def Matrix.PosSemidef {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing 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
Instances For
    source
    theorem Matrix.PosSemidef.diagonal {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] {d : n β†’ R} (h : 0 ≀ d) :
    (Matrix.diagonal d).PosSemidef
    source
    theorem Matrix.posSemidef_diagonal_iff {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] {d : n β†’ R} :
    (Matrix.diagonal d).PosSemidef ↔ βˆ€ (i : n), 0 ≀ d i

    A diagonal matrix is positive semidefinite iff its diagonal entries are nonnegative.

    source
    theorem Matrix.PosSemidef.isHermitian {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] {M : Matrix n n R} (hM : M.PosSemidef) :
    M.IsHermitian
    source
    theorem Matrix.PosSemidef.re_dotProduct_nonneg {n : Type u_2} {π•œ : Type u_4} [Fintype n] [RCLike π•œ] {M : Matrix n n π•œ} (hM : M.PosSemidef) (x : n β†’ π•œ) :
    0 ≀ RCLike.re (Matrix.dotProduct (star x) (M.mulVec x))
    source
    theorem Matrix.PosSemidef.conjTranspose_mul_mul_same {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] {A : Matrix n n R} (hA : A.PosSemidef) {m : Type u_5} [Fintype m] (B : Matrix n m R) :
    (B.conjTranspose * A * B).PosSemidef
    source
    theorem Matrix.PosSemidef.mul_mul_conjTranspose_same {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] {A : Matrix n n R} (hA : A.PosSemidef) {m : Type u_5} [Fintype m] (B : Matrix m n R) :
    (B * A * B.conjTranspose).PosSemidef
    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] [StarRing R] {M : Matrix n n R} (hM : M.PosSemidef) (e : m β†’ n) :
    (M.submatrix e e).PosSemidef
    source
    theorem Matrix.PosSemidef.transpose {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] {M : Matrix n n R} (hM : M.PosSemidef) :
    M.transpose.PosSemidef
    source
    theorem Matrix.PosSemidef.conjTranspose {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] {M : Matrix n n R} (hM : M.PosSemidef) :
    M.conjTranspose.PosSemidef
    source
    theorem Matrix.PosSemidef.zero {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] :
    Matrix.PosSemidef 0
    source
    theorem Matrix.PosSemidef.one {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] :
    Matrix.PosSemidef 1
    source
    theorem Matrix.PosSemidef.natCast {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] (d : β„•) :
    (↑d).PosSemidef
    source
    theorem Matrix.PosSemidef.ofNat {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] (d : β„•) [d.AtLeastTwo] :
    (OfNat.ofNat d).PosSemidef
    source
    theorem Matrix.PosSemidef.intCast {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] (d : β„€) (hd : 0 ≀ d) :
    (↑d).PosSemidef
    source
    @[simp]
    theorem Matrix.posSemidef_intCast_iff {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [Nonempty n] [Nontrivial R] (d : β„€) :
    (↑d).PosSemidef ↔ 0 ≀ d
    source
    theorem Matrix.PosSemidef.pow {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] {M : Matrix n n R} (hM : M.PosSemidef) (k : β„•) :
    (M ^ k).PosSemidef
    source
    theorem Matrix.PosSemidef.inv {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] [DecidableEq n] {M : Matrix n n R} (hM : M.PosSemidef) :
    M⁻¹.PosSemidef
    source
    theorem Matrix.PosSemidef.zpow {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] {M : Matrix n n R} (hM : M.PosSemidef) (z : β„€) :
    (M ^ z).PosSemidef
    source
    theorem Matrix.PosSemidef.add {m : Type u_1} {R : Type u_3} [Fintype m] [CommRing R] [PartialOrder R] [StarRing R] [AddLeftMono R] {A : Matrix m m R} {B : Matrix m m R} (hA : A.PosSemidef) (hB : B.PosSemidef) :
    (A + B).PosSemidef
    source
    theorem Matrix.PosSemidef.eigenvalues_nonneg {n : Type u_2} {π•œ : Type u_4} [Fintype n] [RCLike π•œ] [DecidableEq n] {A : Matrix n n π•œ} (hA : A.PosSemidef) (i : n) :
    0 ≀ β‹―.eigenvalues i

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

    source
    noncomputable def Matrix.PosSemidef.sqrt {n : Type u_2} {π•œ : Type u_4} [Fintype n] [RCLike π•œ] [DecidableEq n] {A : Matrix n n π•œ} (hA : A.PosSemidef) :
    Matrix n n π•œ

    The positive semidefinite square root of a positive semidefinite matrix

    Equations
    Instances For
      source
      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.
      Instances For
        source
        theorem Matrix.PosSemidef.posSemidef_sqrt {n : Type u_2} {π•œ : Type u_4} [Fintype n] [RCLike π•œ] [DecidableEq n] {A : Matrix n n π•œ} (hA : A.PosSemidef) :
        hA.sqrt.PosSemidef
        source
        @[simp]
        theorem Matrix.PosSemidef.sq_sqrt {n : Type u_2} {π•œ : Type u_4} [Fintype n] [RCLike π•œ] [DecidableEq n] {A : Matrix n n π•œ} (hA : A.PosSemidef) :
        hA.sqrt ^ 2 = A
        source
        @[simp]
        theorem Matrix.PosSemidef.sqrt_mul_self {n : Type u_2} {π•œ : Type u_4} [Fintype n] [RCLike π•œ] [DecidableEq n] {A : Matrix n n π•œ} (hA : A.PosSemidef) :
        hA.sqrt * hA.sqrt = A
        source
        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 : A.PosSemidef) {B : Matrix n n π•œ} (hB : B.PosSemidef) (hAB : A ^ 2 = B ^ 2) :
        A = B
        source
        theorem Matrix.PosSemidef.sqrt_sq {n : Type u_2} {π•œ : Type u_4} [Fintype n] [RCLike π•œ] [DecidableEq n] {A : Matrix n n π•œ} (hA : A.PosSemidef) :
        (β‹― : (A ^ 2).PosSemidef).sqrt = A
        source
        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 : A.PosSemidef) {B : Matrix n n π•œ} (hB : B.PosSemidef) (hAB : A ^ 2 = B) :
        A = hB.sqrt
        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] [StarRing R] {M : Matrix n n R} (e : m ≃ n) :
        (M.submatrix ⇑e ⇑e).PosSemidef ↔ M.PosSemidef
        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] [StarRing R] [StarOrderedRing R] (A : Matrix m n R) :
        (A.conjTranspose * A).PosSemidef

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

        A matrix multiplied by its conjugate transpose is positive semidefinite

        source
        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 ≀ β‹―.eigenvalues i
        source
        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 ≀ β‹―.eigenvalues i
        source
        theorem Matrix.posSemidef_iff_eq_transpose_mul_self {n : Type u_2} {π•œ : Type u_4} [Fintype n] [RCLike π•œ] {A : Matrix n n π•œ} :
        A.PosSemidef ↔ βˆƒ (B : Matrix n n π•œ), A = B.conjTranspose * B

        A matrix is positive semidefinite if and only if it has the form Bα΄΄ * B for some B.

        source
        theorem Matrix.IsHermitian.posSemidef_of_eigenvalues_nonneg {n : Type u_2} {π•œ : Type u_4} [Fintype n] [RCLike π•œ] [DecidableEq n] {A : Matrix n n π•œ} (hA : A.IsHermitian) (h : βˆ€ (i : n), 0 ≀ hA.eigenvalues i) :
        A.PosSemidef
        source
        theorem Matrix.PosSemidef.dotProduct_mulVec_zero_iff {n : Type u_2} {π•œ : Type u_4} [Fintype n] [RCLike π•œ] {A : Matrix n n π•œ} (hA : A.PosSemidef) (x : n β†’ π•œ) :
        Matrix.dotProduct (star x) (A.mulVec x) = 0 ↔ A.mulVec x = 0

        For A positive semidefinite, we have x⋆ A x = 0 iff A x = 0.

        source
        theorem Matrix.PosSemidef.toLinearMapβ‚‚'_zero_iff {n : Type u_2} {π•œ : Type u_4} [Fintype n] [RCLike π•œ] [DecidableEq n] {A : Matrix n n π•œ} (hA : A.PosSemidef) (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 #

        source
        def Matrix.PosDef {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing 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
        Instances For
          source
          theorem Matrix.PosDef.isHermitian {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] {M : Matrix n n R} (hM : M.PosDef) :
          M.IsHermitian
          source
          theorem Matrix.PosDef.re_dotProduct_pos {n : Type u_2} {π•œ : Type u_4} [Fintype n] [RCLike π•œ] {M : Matrix n n π•œ} (hM : M.PosDef) {x : n β†’ π•œ} (hx : x β‰  0) :
          0 < RCLike.re (Matrix.dotProduct (star x) (M.mulVec x))
          source
          theorem Matrix.PosDef.posSemidef {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] {M : Matrix n n R} (hM : M.PosDef) :
          M.PosSemidef
          source
          theorem Matrix.PosDef.transpose {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] {M : Matrix n n R} (hM : M.PosDef) :
          M.transpose.PosDef
          source
          theorem Matrix.PosDef.diagonal {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] {d : n β†’ R} (h : βˆ€ (i : n), 0 < d i) :
          (Matrix.diagonal d).PosDef
          source
          @[simp]
          theorem Matrix.posDef_diagonal_iff {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] [Nontrivial R] {d : n β†’ R} :
          (Matrix.diagonal d).PosDef ↔ βˆ€ (i : n), 0 < d i
          source
          theorem Matrix.PosDef.one {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] :
          Matrix.PosDef 1
          source
          theorem Matrix.PosDef.natCast {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] (d : β„•) (hd : d β‰  0) :
          (↑d).PosDef
          source
          @[simp]
          theorem Matrix.posDef_natCast_iff {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] [Nonempty n] [Nontrivial R] {d : β„•} :
          (↑d).PosDef ↔ 0 < d
          source
          theorem Matrix.PosDef.ofNat {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] (d : β„•) [d.AtLeastTwo] :
          (OfNat.ofNat d).PosDef
          source
          theorem Matrix.PosDef.intCast {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] (d : β„€) (hd : 0 < d) :
          (↑d).PosDef
          source
          @[simp]
          theorem Matrix.posDef_intCast_iff {n : Type u_2} {R : Type u_3} [Fintype n] [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] [Nonempty n] [Nontrivial R] {d : β„€} :
          (↑d).PosDef ↔ 0 < d
          source
          theorem Matrix.PosDef.add_posSemidef {m : Type u_1} {R : Type u_3} [Fintype m] [CommRing R] [PartialOrder R] [StarRing R] [AddLeftMono R] {A : Matrix m m R} {B : Matrix m m R} (hA : A.PosDef) (hB : B.PosSemidef) :
          (A + B).PosDef
          source
          theorem Matrix.PosDef.posSemidef_add {m : Type u_1} {R : Type u_3} [Fintype m] [CommRing R] [PartialOrder R] [StarRing R] [AddLeftMono R] {A : Matrix m m R} {B : Matrix m m R} (hA : A.PosSemidef) (hB : B.PosDef) :
          (A + B).PosDef
          source
          theorem Matrix.PosDef.add {m : Type u_1} {R : Type u_3} [Fintype m] [CommRing R] [PartialOrder R] [StarRing R] [AddLeftMono R] {A : Matrix m m R} {B : Matrix m m R} (hA : A.PosDef) (hB : B.PosDef) :
          (A + B).PosDef
          source
          theorem Matrix.PosDef.of_toQuadraticForm' {n : Type u_2} [Fintype n] [DecidableEq n] {M : Matrix n n ℝ} (hM : M.IsSymm) (hMq : M.toQuadraticMap'.PosDef) :
          M.PosDef
          source
          theorem Matrix.PosDef.toQuadraticForm' {n : Type u_2} [Fintype n] [DecidableEq n] {M : Matrix n n ℝ} (hM : M.PosDef) :
          M.toQuadraticMap'.PosDef
          source
          theorem Matrix.PosDef.eigenvalues_pos {n : Type u_2} {π•œ : Type u_4} [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

          source
          theorem Matrix.PosDef.det_pos {n : Type u_2} {π•œ : Type u_4} [Fintype n] [RCLike π•œ] [DecidableEq n] {M : Matrix n n π•œ} (hM : M.PosDef) :
          0 < M.det
          source
          theorem Matrix.PosDef.isUnit {n : Type u_2} {π•œ : Type u_4} [Fintype n] [RCLike π•œ] [DecidableEq n] {M : Matrix n n π•œ} (hM : M.PosDef) :
          IsUnit M
          source
          theorem Matrix.PosDef.inv {n : Type u_2} {π•œ : Type u_4} [Fintype n] [RCLike π•œ] [DecidableEq n] {M : Matrix n n π•œ} (hM : M.PosDef) :
          M⁻¹.PosDef
          source
          @[simp]
          theorem Matrix.posDef_inv_iff {n : Type u_2} {π•œ : Type u_4} [Fintype n] [RCLike π•œ] [DecidableEq n] {M : Matrix n n π•œ} :
          M⁻¹.PosDef ↔ M.PosDef
          source
          theorem QuadraticForm.posDef_of_toMatrix' {n : Type u_1} [Fintype n] [DecidableEq n] {Q : QuadraticForm ℝ (n β†’ ℝ)} (hQ : (QuadraticMap.toMatrix' Q).PosDef) :
          QuadraticMap.PosDef Q
          source
          theorem QuadraticForm.posDef_toMatrix' {n : Type u_1} [Fintype n] [DecidableEq n] {Q : QuadraticForm ℝ (n β†’ ℝ)} (hQ : QuadraticMap.PosDef Q) :
          (QuadraticMap.toMatrix' Q).PosDef
          source
          @[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
            source
            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