Documentation

OptimizationTheoryAndMethods_SunYuan_2006.Chap01.Definition_1_2_8

source
@[reducible, inline]
abbrev Matrix.NegDef {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) :
Prop

Chapter01 Definition 1.2.8 (1): for a symmetric real square matrix A, negative definiteness means that -A is positive definite.

Instances For
    source
    @[simp]
    theorem Matrix.negDef_iff {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} :
    A.NegDef ↔ (-A).PosDef

    Characterization of Matrix.NegDef.

    source
    @[reducible, inline]
    abbrev Matrix.NegSemidef {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) :
    Prop

    Chapter01 Definition 1.2.8 (2): for a symmetric real square matrix A, negative semidefiniteness means that -A is positive semidefinite.

    Instances For
      source
      @[simp]
      theorem Matrix.negSemidef_iff {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} :
      A.NegSemidef ↔ (-A).PosSemidef

      Characterization of Matrix.NegSemidef.

      source
      theorem Matrix.NegDef.isSymm {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} (hA : A.NegDef) :
      A.IsSymm

      A negative definite real matrix is symmetric.

      source
      theorem Matrix.NegDef.negSemidef {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} (hA : A.NegDef) :
      A.NegSemidef

      A negative definite real matrix is negative semidefinite.

      source
      theorem Matrix.NegSemidef.isSymm {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} (hA : A.NegSemidef) :
      A.IsSymm

      A negative semidefinite real matrix is symmetric.

      source
      class Matrix.Indefinite {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) :
      Prop

      Chapter01 Definition 1.2.8 (3): a symmetric real square matrix is indefinite if it is neither positive semidefinite nor negative semidefinite.

      • isSymm : A.IsSymm
      • not_posSemidef : ¬A.PosSemidef
      • not_negSemidef : ¬A.NegSemidef
      Instances
        source
        @[implicit_reducible]
        noncomputable instance Matrix.instDecidableIndefinite {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) :
        Decidable A.Indefinite

        Indefiniteness of a real square matrix is classically decidable.

        source
        @[simp]
        theorem Matrix.indefinite_iff {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} :
        A.Indefinite ↔ A.IsSymm ∧ ¬A.PosSemidef ∧ ¬A.NegSemidef

        Characterization of Matrix.Indefinite.

        source
        theorem Matrix.Indefinite.not_posDef {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} (hA : A.Indefinite) :
        ¬A.PosDef

        An indefinite real matrix cannot be positive definite.

        source
        theorem Matrix.Indefinite.not_negDef {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} (hA : A.Indefinite) :
        ¬A.NegDef

        An indefinite real matrix cannot be negative definite.