Reference · Matrices

rainbow.math.linear.matrix.prepend-add

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

Shape-safe additivity of total column insertion. Under matching vector and matrix shapes, matrix/prepend-column preserves the resulting matrix shape and distributes over vector/matrix addition. A joint theorem shares the required four-list induction; public projections expose the shape and equivalence facts separately. Native and axiom-free on D63.

Depends onmath.linear.matrix.add-shape

matrix/prepend-column-additive-with-shape :
  (left-values right-values : List ℚ) (left-columns right-columns : List (List ℚ))
  (values-shape : vector/same-shape left-values right-values)
  (columns-shape : matrix/same-shape left-columns right-columns)
  → proposition/conjunction (shape) (equivalent)
  where equivalent := matrix/equivalent (matrix/prepend-column (vector/add left-values right-values) (matrix/add left-columns right-columns)) (matrix/add (matrix/prepend-column left-values left-columns) (matrix/prepend-column right-values right-columns))
  where shape := matrix/same-shape (matrix/prepend-column left-values left-columns) (matrix/prepend-column right-values right-columns)

matrix/prepend-column-preserves-same-shape :
  (left-values right-values : List ℚ) (left-columns right-columns : List (List ℚ))
  (values-shape : vector/same-shape left-values right-values)
  (columns-shape : matrix/same-shape left-columns right-columns)
  → matrix/same-shape (column₁) (column)
  where column := matrix/prepend-column right-values right-columns
  where column₁ := matrix/prepend-column left-values left-columns

matrix/prepend-column-additive :
  (left-values right-values : List ℚ) (left-columns right-columns : List (List ℚ))
  (values-shape : vector/same-shape left-values right-values)
  (columns-shape : matrix/same-shape left-columns right-columns)
  → matrix/equivalent (column) (add)
  where add := matrix/add (matrix/prepend-column left-values left-columns) (matrix/prepend-column right-values right-columns)
  where column := matrix/prepend-column (vector/add left-values right-values) (matrix/add left-columns right-columns)