Reference · Matrices

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

Matricessrc/rainbow/math/linear/matrix/least_squares_normal.clj0 definitions, 3 theorems

Normal-equation sufficiency for exact finite least squares. If a residual r has the output shape of A and A^T r is componentwise zero, adjointness makes r orthogonal to every compatible image A d. Pythagoras then gives the exact affine decomposition ||r + A d||^2 = ||r||^2 + ||A d||^2 and hence ||r||^2 <= ||r + A d||^2. This is the native exact-rational normal-equation optimality theorem, with all row-list shape assumptions explicit. Theorem-only, kernel-checked, and axiom-free on D63.

Depends onmath.linear.vector.norm-pythagorean

matrix/transpose-null-orthogonal-image :
  (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)))
  → vector/dot residual (matrix/vector-multiply rows direction) = 0
  where multiply := matrix/vector-multiply (matrix/transpose rows) residual

matrix/normal-residual-affine-pythagorean :
  (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)))
  → norm/norm-squared (vector/add residual (matrix/vector-multiply rows direction)) = norm/norm-squared residual + norm/norm-squared (matrix/vector-multiply rows direction)
  where multiply := matrix/vector-multiply (matrix/transpose rows) residual

matrix/normal-residual-affine-optimal :
  (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)))
  → norm/norm-squared residual ≤ norm/norm-squared (vector/add residual (matrix/vector-multiply rows direction))
  where multiply := matrix/vector-multiply (matrix/transpose rows) residual