Reference · Matrices

rainbow.math.linear.matrix.action-sup-bound

Matricessrc/rainbow/math/linear/matrix/action_sup_bound.clj0 definitions, 1 theorems

Lift rowwise dot-distance bounds to a matrix-action sup bound. Matrix-vector multiplication maps dot product over the row list. If every member row moves two inputs by at most a common signed upper bound, and zero is below that bound, structural induction shows the whole output vector is within the same sup-distance bound. This separates the generic operator lift from later row-norm or stochastic-row certificates. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.matrixmath.rational.signed.vector-sup-distance

matrix/vector-multiply-sup-distance-bounded :
  (rows : List (List ℚ)) (left right : List ℚ) (upper : ℚ)
  (zero-upper : 0 ≤ upper)
  (rowwise : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) rows row), signed/distance (vector/dot row left) (vector/dot row right) ≤ upper)
  → vector/sup-distance (matrix/vector-multiply rows left) (matrix/vector-multiply rows right) ≤ upper