Reference · Matrices

rainbow.math.linear.matrix.action-prepend

Matricessrc/rainbow/math/linear/matrix/action_prepend.clj0 definitions, 5 theorems

Action laws for inserting a leading column into a native finite matrix. Acting on a column inserted into no prior columns yields exactly the signed scaling of that column. With existing columns, equal row/column count is the necessary premise for the usual decomposition into the scaled inserted column plus the old matrix action; without it native vector/add truncation makes the statement false. Native and axiom-free on D63.

Depends onmath.linear.matrix.action-scale

signed/multiply-to-scale-difference :
  (value factor : ℚ)
  → value · factor = signed/scale (signed/positive factor) value - signed/scale (signed/negative factor) value

signed/prepend-action-head :
  (value factor tail-product : ℚ)
  → value · factor + tail-product = signed/scale (signed/positive factor) value - signed/scale (signed/negative factor) value + tail-product

signed/prepend-action-empty-head :
  (value factor : ℚ)
  → value · factor + 0 = signed/scale (signed/positive factor) value - signed/scale (signed/negative factor) value

matrix/vector-multiply-prepend-column-empty :
  (factor : ℚ) (values weights : List ℚ)
  → vector/equivalent (multiply) (vector/signed-scale factor values)
  where multiply := matrix/vector-multiply (matrix/prepend-column values []) (data/cons ℚ factor weights)

matrix/vector-multiply-prepend-column :
  (factor : ℚ) (values : List ℚ) (columns : List (List ℚ)) (weights : List ℚ)
  (shape : vector/same-shape values (matrix/column-shape columns))
  → vector/equivalent (multiply) (add)
  where add := vector/add (vector/signed-scale factor values) (matrix/vector-multiply columns weights)
  where multiply := matrix/vector-multiply (matrix/prepend-column values columns) (data/cons ℚ factor weights)