Sylvester's criterion

DefinitionLeading principal submatrix#✓fully proved

The leading k × k principal submatrix of A: the submatrix on the first k rows and columns.

def leadingPrincipalSubmatrix {α : Type*} {n : ℕ} (A : Matrix (Fin n) (Fin n) α)
    (k : ℕ) (hk : k ≤ n) : Matrix (Fin k) (Fin k) α :=
  A.submatrix (Fin.castLE hk) (Fin.castLE hk)

Used by 2

Used byFull leading principal submatrix is the matrix itself · Sylvester's criterion

TheoremFull leading principal submatrix is the matrix itself#✓fully proved

The full leading principal submatrix is the matrix itself.

theorem leadingPrincipalSubmatrix_self {α : Type*} {n : ℕ}
    (A : Matrix (Fin n) (Fin n) α) :
    leadingPrincipalSubmatrix A n (Nat.le_refl n) = A

Uses 1 · Used by 1

Statement usesLeading principal submatrix

Used bySylvester's criterion

TheoremPositive definiteness of a block matrix via the Schur complement#✓fully proved

A block matrix with a positive definite top-left block and a positive definite Schur complement is positive definite. This is the one-step induction step of Sylvester's criterion, stated for a 1 × 1 bottom-right block.

theorem PosDef.fromBlocks {n : ℕ} {B : Matrix (Fin n) (Fin n) ℝ}
    {u : Matrix (Fin n) (Fin 1) ℝ} {D : Matrix (Fin 1) (Fin 1) ℝ}
    (hB : B.PosDef) (hD : D.IsHermitian)
    (hS : (D - uᴴ * B⁻¹ * u).PosDef) :
    (Matrix.fromBlocks B u uᴴ D).PosDef

Used by 1

Used bySylvester's criterion

TheoremSylvester's criterion#✓fully proved

A Hermitian real matrix is positive definite if and only if all of its leading principal minors are positive. The Hermitian hypothesis is essential: !![1, 2; 0, 1] has leading minors 1 and 1 but is not Hermitian, hence not positive definite.

theorem posDef_iff_leadingPrincipalMinors_pos :
    ∀ (n : ℕ) (A : Matrix (Fin n) (Fin n) ℝ), A.IsHermitian →
      (A.PosDef ↔ ∀ (k : ℕ) (hk : k ≤ n),
        0 < (leadingPrincipalSubmatrix A k hk).det)

Uses 3

Statement usesLeading principal submatrix

Proof usesPositive definiteness of a block matrix via the Schur complement · Full leading principal submatrix is the matrix itself

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.