Reference · Matrices

rainbow.math.linear.matrix.signed-scale-algebra

Matricessrc/rainbow/math/linear/matrix/signed_scale_algebra.clj0 definitions, 6 theorems

Additivity and composition of arbitrary signed matrix scaling. The scale-difference representation is additive in its value and composes by signed multiplication. Structural lifts give the corresponding laws for vector/signed-scale and matrix/signed-scale. Additivity carries the exact length-sensitive shape premise required by truncating addition; composition is unrestricted. Native and axiom-free on D63.

Depends onmath.linear.matrix.subtract-linear

signed/scale-difference-additive :
  (factor left right : ℚ)
  → signed/scale (signed/positive factor) (left + right) - signed/scale (signed/negative factor) (left + right) = signed/scale (signed/positive factor) left - signed/scale (signed/negative factor) left + (signed/scale (signed/positive factor) right - signed/scale (signed/negative factor) right)

signed/scale-difference-compose :
  (outer inner value : ℚ)
  → signed/scale (signed/positive outer) (scale - scale₁) - signed/scale (signed/negative outer) (scale - scale₁) = signed/scale (signed/positive (outer · inner)) value - signed/scale (signed/negative (outer · inner)) value
  where scale := signed/scale (signed/positive inner) value
  where scale₁ := signed/scale (signed/negative inner) value

vector/signed-scale-additive :
  (factor : ℚ) (left right : List ℚ) (shape : vector/same-shape left right)
  → vector/equivalent (scale) (add)
  where add := vector/add (vector/signed-scale factor left) (vector/signed-scale factor right)
  where scale := vector/signed-scale factor (vector/add left right)

vector/signed-scale-compose :
  (outer inner : ℚ) (values : List ℚ)
  → vector/equivalent (scale) (scale₁)
  where scale := vector/signed-scale outer (vector/signed-scale inner values)
  where scale₁ := vector/signed-scale (outer · inner) values

matrix/signed-scale-additive :
  (factor : ℚ) (left right : List (List ℚ)) (shape : matrix/same-shape left right)
  → matrix/equivalent (scale) (add)
  where add := matrix/add (matrix/signed-scale factor left) (matrix/signed-scale factor right)
  where scale := matrix/signed-scale factor (matrix/add left right)

matrix/signed-scale-compose :
  (outer inner : ℚ) (rows : List (List ℚ))
  → matrix/equivalent (scale) (scale₁)
  where scale := matrix/signed-scale outer (matrix/signed-scale inner rows)
  where scale₁ := matrix/signed-scale (outer · inner) rows