Reference · Matrices

rainbow.math.linear.matrix.action-scale

Matricessrc/rainbow/math/linear/matrix/action_scale.clj1 definitions, 4 theorems

Arbitrary signed-scalar vector scaling for native matrix algebra. A signed rational is represented by its nonnegative positive and negative components. Its vector action is therefore the difference between those two native nonnegative vector scalings. This is definitionally the pointwise signed product, while exposing enough existing linear algebra to derive dot homogeneity without an expensive nested List induction. Native and axiom-free on D63.

Depends onmath.linear.matrix.composable-multiplymath.linear.vector.dot-subtractmath.linear.vector.dot-scalemath.linear.vector.shape-add

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

signed/multiply-distributes-add-left :
  (factor left right : ℚ)
  → factor · (left + right) = factor · left + factor · right

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

vector/signed-scale-preserves-shape :
  (factor : ℚ) (values : List ℚ)
  → vector/same-shape (vector/signed-scale factor values) values

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