Reference · Matrices

rainbow.math.linear.matrix.multiply-associative

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

Associativity of composable native finite matrix multiplication. For a nonempty middle matrix, composability of A*B and B*C entails (A*B)*C ~ A*(B*C). The nonempty premise is exact for the row-list representation: an empty middle matrix can erase an output width that a later multiplication would otherwise recover. The proof lifts transpose/action associativity across explicit columns, transports through the certified transpose/product bridge, and then maps the row theorem over A. Native and axiom-free on D63.

Depends onmath.linear.matrix.transpose-multiply

matrix/vector-multiply-column-action-associative :
  (rows columns : List (List ℚ)) (coefficients reference : List ℚ)
  (coefficient-shape : vector/same-shape coefficients (matrix/column-shape rows))
  (rows-compatible : matrix/compatible rows reference)
  (columns-compatible : matrix/compatible columns reference)
  → vector/equivalent (multiply) (multiply₁)
  where multiply := matrix/vector-multiply columns (matrix/vector-multiply (matrix/transpose rows) coefficients)
  where multiply₁ := matrix/vector-multiply (matrix/column-action rows columns) coefficients

matrix/multiply-row-associative :
  (middle-head : List ℚ) (middle-tail right : List (List ℚ))
  (coefficients reference : List ℚ)
  (coefficient-shape : vector/same-shape coefficients (matrix/column-shape (data/cons (List ℚ) middle-head middle-tail)))
  (middle-compatible : matrix/compatible (data/cons (List ℚ) middle-head middle-tail) reference)
  (columns-compatible : matrix/compatible (matrix/transpose right) reference)
  → vector/equivalent (multiply) (multiply₁)
  where multiply := matrix/vector-multiply (matrix/transpose right) (matrix/vector-multiply (matrix/transpose (data/cons (List ℚ) middle-head middle-tail)) coefficients)
  where multiply₁ := matrix/vector-multiply (matrix/transpose (matrix/multiply (data/cons (List ℚ) middle-head middle-tail) right)) coefficients

matrix/multiply-associative-nonempty-middle :
  (left : List (List ℚ)) (middle-head : List ℚ) (middle-tail right : List (List ℚ))
  (left-middle-composable : matrix/composable left (data/cons (List ℚ) middle-head middle-tail))
  (middle-right-composable : matrix/composable (data/cons (List ℚ) middle-head middle-tail) right)
  → matrix/equivalent (multiply₁) (multiply)
  where multiply := matrix/multiply left (matrix/multiply (data/cons (List ℚ) middle-head middle-tail) right)
  where multiply₁ := matrix/multiply (matrix/multiply left (data/cons (List ℚ) middle-head middle-tail)) right