Reference · Matrices

rainbow.math.linear.matrix.gram-positive

Matricessrc/rainbow/math/linear/matrix/gram_positive.clj0 definitions, 3 theorems

Positive-semidefinite Gram action for native signed matrices. Every signed vector has a nonnegative self-dot, without an entrywise sign premise. The checked transpose/action adjoint law identifies the quadratic action dot((A^T)(Ax), x) with dot(Ax, Ax), so the Gram quadratic form is nonnegative for every vector compatible with A. This is the exact-rational positive-semidefinite bridge needed by least-squares and quadratic OR cones. Native and axiom-free on D63.

Depends onmath.linear.matrix.positive-multiply

vector/dot-self-nonnegative :
  (values : List ℚ)
  → 0 ≤ vector/dot values values

matrix/gram-action-equivalent-dot-self :
  (rows : List (List ℚ)) (values : List ℚ)
  (rows-compatible : matrix/compatible rows values)
  → vector/dot (multiply) values = vector/dot (matrix/vector-multiply rows values) (matrix/vector-multiply rows values)
  where multiply := matrix/vector-multiply (matrix/transpose rows) (matrix/vector-multiply rows values)

matrix/gram-action-nonnegative :
  (rows : List (List ℚ)) (values : List ℚ)
  (rows-compatible : matrix/compatible rows values)
  → 0 ≤ vector/dot (multiply) values
  where multiply := matrix/vector-multiply (matrix/transpose rows) (matrix/vector-multiply rows values)