Reference · Matrices

rainbow.math.linear.matrix.affine-sup-distance

Matricessrc/rainbow/math/linear/matrix/affine_sup_distance.clj0 definitions, 2 theorems

Sup-distance cancellation and bound transfer for signed affine action. Matrix-vector output length depends only on the row list. Consequently one certificate that the affine offset has the action-output shape also covers every other input to the same matrix. Fixed-shape vector translation then cancels the common offset exactly, and the order corollary transfers any linear-action distance bound to the affine map. Native, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-ordermath.linear.matrix.linearmath.rational.signed.vector-sup-translation

matrix/affine-action-sup-distance-cancels-offset :
  (rows : List (List ℚ)) (offset left right : List ℚ)
  (offset-shape : vector/same-shape offset (matrix/vector-multiply rows left))
  → vector/sup-distance (matrix/affine-action rows offset left) (matrix/affine-action rows offset right) = vector/sup-distance (matrix/vector-multiply rows left) (matrix/vector-multiply rows right)

matrix/affine-action-sup-distance-bounded :
  (rows : List (List ℚ)) (offset left right : List ℚ) (upper : ℚ)
  (offset-shape : vector/same-shape offset (matrix/vector-multiply rows left))
  (linear-bound : vector/sup-distance (matrix/vector-multiply rows left) (matrix/vector-multiply rows right) ≤ upper)
  → vector/sup-distance (matrix/affine-action rows offset left) (matrix/affine-action rows offset right) ≤ upper