Reference · Matrices

rainbow.math.linear.matrix.row-gram

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

Symmetry and positive semidefiniteness of the native row Gram product. For a rectangular matrix A with an explicitly nonempty first row, total transpose is involutive. Consequently AA^T is symmetric, and its quadratic action is equivalent to the self-dot of A^T x. The latter is nonnegative for arbitrary signed entries. The positive-width premise is mathematically exact for Rainbow's row-list encoding, which forgets nonempty zero-width matrices under transpose. Native and axiom-free on D63.

Depends onmath.linear.matrix.gram-kernel

matrix/row-gram-symmetric-positive-width :
  (head : ℚ) (row-tail : List ℚ) (tail : List (List ℚ))
  (rows-rectangular : matrix/rectangular (data/cons (List ℚ) (data/cons ℚ head row-tail) tail))
  → matrix/equivalent (matrix/transpose (multiply)) (multiply)
  where multiply := matrix/multiply (data/cons (List ℚ) (data/cons ℚ head row-tail) tail) (matrix/transpose (data/cons (List ℚ) (data/cons ℚ head row-tail) tail))

matrix/row-gram-action-equivalent-dot-self :
  (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)
  → vector/dot (multiply) values = vector/dot (matrix/vector-multiply (matrix/transpose (data/cons (List ℚ) (data/cons ℚ head row-tail) tail)) values) (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-nonnegative :
  (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)
  → 0 ≤ vector/dot (multiply) 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)