Reference · Matrices

rainbow.math.linear.matrix.least-squares-equality

Matricessrc/rainbow/math/linear/matrix/least_squares_equality.clj0 definitions, 5 theorems

Equality and nullspace directions in exact finite least squares. Signed additive equivalence cancellation is derived from the existing order cancellation laws and antisymmetry. Applying it to the normal-residual Pythagorean identity proves that the affine least-squares objective equals its normal residual value exactly when A d is componentwise zero. Thus normal solutions are unique modulo ker A, with all finite row-list shape premises explicit. Theorem-only, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.least-squares-normal

signed/equivalent-add-right-cancel :
  (left right offset : ℚ)
  (same : left + offset = right + offset)
  → left = right

signed/equivalent-add-left-cancel :
  (left right offset : ℚ)
  (same : offset + left = offset + right)
  → left = right

matrix/normal-affine-equal-of-null-direction :
  (rows : List (List ℚ)) (residual direction : List ℚ)
  (residual-shape : vector/same-shape residual (matrix/column-shape rows))
  (direction-compatible : matrix/compatible rows direction)
  (transpose-null : vector/equivalent (multiply) (vector/zero-like (multiply)))
  (direction-null : vector/equivalent (matrix/vector-multiply rows direction) (vector/zero-like (matrix/vector-multiply rows direction)))
  → norm/norm-squared (vector/add residual (matrix/vector-multiply rows direction)) = norm/norm-squared residual
  where multiply := matrix/vector-multiply (matrix/transpose rows) residual

matrix/normal-affine-equal-reflects-null-direction :
  (rows : List (List ℚ)) (residual direction : List ℚ)
  (residual-shape : vector/same-shape residual (matrix/column-shape rows))
  (direction-compatible : matrix/compatible rows direction)
  (transpose-null : vector/equivalent (multiply) (vector/zero-like (multiply)))
  (objective-equal : norm/norm-squared (vector/add residual (matrix/vector-multiply rows direction)) = norm/norm-squared residual)
  → vector/equivalent (matrix/vector-multiply rows direction) (vector/zero-like (matrix/vector-multiply rows direction))
  where multiply := matrix/vector-multiply (matrix/transpose rows) residual

matrix/normal-affine-equality-characterizes-null-direction :
  (rows : List (List ℚ)) (residual direction : List ℚ)
  (residual-shape : vector/same-shape residual (matrix/column-shape rows))
  (direction-compatible : matrix/compatible rows direction)
  (transpose-null : vector/equivalent (multiply) (vector/zero-like (multiply)))
  → proposition/conjunction (norm/norm-squared (add) = norm/norm-squared residual → equivalent) (equivalent → norm/norm-squared (add) = norm/norm-squared residual)
  where add := vector/add residual (matrix/vector-multiply rows direction)
  where equivalent := vector/equivalent (matrix/vector-multiply rows direction) (vector/zero-like (matrix/vector-multiply rows direction))
  where multiply := matrix/vector-multiply (matrix/transpose rows) residual