Reference · Matrices

rainbow.math.linear.matrix.signed-scale

Matricessrc/rainbow/math/linear/matrix/signed_scale.clj1 definitions, 3 theorems

Arbitrary signed-scalar homogeneity for native finite matrices. The existing vector/signed-scale acts pointwise by an arbitrary signed rational. Dot products are homogeneous in their second argument as well as their first, so native matrix action commutes with scaling its input. Mapping the same action over matrix rows then gives an unrestricted left-factor homogeneity law for matrix multiplication. These laws remain valid for ragged and empty matrices because every operation uses the same total list semantics. Native and axiom-free on D63.

Depends onmath.linear.matrix.associativity-counterexample

matrix/signed-scale :
  (x₁ : ℚ) (x₂ : List (List ℚ))
  → List (List ℚ)

vector/dot-signed-scale-right :
  (factor : ℚ) (values weights : List ℚ)
  → vector/dot values (vector/signed-scale factor weights) = factor · vector/dot values weights

matrix/vector-multiply-signed-scale :
  (factor : ℚ) (rows : List (List ℚ)) (values : List ℚ)
  → vector/equivalent (multiply) (scale)
  where multiply := matrix/vector-multiply rows (vector/signed-scale factor values)
  where scale := vector/signed-scale factor (matrix/vector-multiply rows values)

matrix/multiply-signed-scale-left :
  (factor : ℚ) (left right : List (List ℚ))
  → matrix/equivalent (multiply) (scale)
  where multiply := matrix/multiply (matrix/signed-scale factor left) right
  where scale := matrix/signed-scale factor (matrix/multiply left right)