Reference · Matrices

rainbow.math.linear.matrix.row-gram-kernel

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

Zero-kernel characterization for the native row Gram product AA^T. Under the exact rectangular positive-width and compatibility premises used by the row-Gram identity, x^T AA^T x is zero exactly when A^T x is componentwise equivalent to its shape-preserving zero vector. Both implications and their conjunction are ordinary theorem data, kernel-checked and axiom-free on D63.

Depends onmath.linear.matrix.row-gram

matrix/row-gram-action-zero-of-transpose-null :
  (head : ℚ) (row-tail : List ℚ) (tail : List (List ℚ)) (values : List ℚ)
  (rows-rectangular : matrix/rectangular (data/cons (List ℚ) (data/cons ℚ head row-tail) tail))
  (transpose-compatible : matrix/compatible (matrix/transpose (data/cons (List ℚ) (data/cons ℚ head row-tail) tail)) values)
  (transpose-image-zero : vector/equivalent (matrix/vector-multiply (matrix/transpose (data/cons (List ℚ) (data/cons ℚ head row-tail) tail)) values) (vector/zero-like (matrix/vector-multiply (matrix/transpose (data/cons (List ℚ) (data/cons ℚ head row-tail) tail)) values)))
  → vector/dot (multiply) values = 0
  where multiply := matrix/vector-multiply (data/cons (List ℚ) (data/cons ℚ head row-tail) tail) (matrix/vector-multiply (matrix/transpose (data/cons (List ℚ) (data/cons ℚ head row-tail) tail)) values)

matrix/row-gram-action-zero-reflects-transpose-null :
  (head : ℚ) (row-tail : List ℚ) (tail : List (List ℚ)) (values : List ℚ)
  (rows-rectangular : matrix/rectangular (data/cons (List ℚ) (data/cons ℚ head row-tail) tail))
  (transpose-compatible : matrix/compatible (matrix/transpose (data/cons (List ℚ) (data/cons ℚ head row-tail) tail)) values)
  (quadratic-zero : vector/dot (multiply) values = 0)
  → vector/equivalent (matrix/vector-multiply (matrix/transpose (data/cons (List ℚ) (data/cons ℚ head row-tail) tail)) values) (vector/zero-like (matrix/vector-multiply (matrix/transpose (data/cons (List ℚ) (data/cons ℚ head row-tail) tail)) values))
  where multiply := matrix/vector-multiply (data/cons (List ℚ) (data/cons ℚ head row-tail) tail) (matrix/vector-multiply (matrix/transpose (data/cons (List ℚ) (data/cons ℚ head row-tail) tail)) values)

matrix/row-gram-action-zero-characterizes-transpose-null :
  (head : ℚ) (row-tail : List ℚ) (tail : List (List ℚ)) (values : List ℚ)
  (rows-rectangular : matrix/rectangular (data/cons (List ℚ) (data/cons ℚ head row-tail) tail))
  (transpose-compatible : matrix/compatible (matrix/transpose (data/cons (List ℚ) (data/cons ℚ head row-tail) tail)) values)
  → proposition/conjunction (dot = 0 → equivalent) (equivalent → dot = 0)
  where dot := vector/dot (matrix/vector-multiply (data/cons (List ℚ) (data/cons ℚ head row-tail) tail) (matrix/vector-multiply (matrix/transpose (data/cons (List ℚ) (data/cons ℚ head row-tail) tail)) values)) values
  where equivalent := vector/equivalent (matrix/vector-multiply (matrix/transpose (data/cons (List ℚ) (data/cons ℚ head row-tail) tail)) values) (vector/zero-like (matrix/vector-multiply (matrix/transpose (data/cons (List ℚ) (data/cons ℚ head row-tail) tail)) values))