Reference · Vectors

rainbow.math.linear.vector.norm-pythagorean

Vectorssrc/rainbow/math/linear/vector/norm_pythagorean.clj0 definitions, 3 theorems

Pythagoras and order bounds for native signed-rational vectors. For same-shaped vectors with zero inner product, the existing four-term norm expansion collapses to the exact sum of the two squared norms. Since every self-dot is nonnegative, either summand's squared norm is at most the squared norm of the orthogonal sum. These theorem-only boundaries are the generic bridge from Gram positivity to least-squares optimality. Native and axiom-free on D63.

Depends onmath.linear.matrix.row-gram-kernel

norm/norm-squared-add-orthogonal :
  (left right : List ℚ) (shape : vector/same-shape left right)
  (orthogonal : vector/dot left right = 0)
  → norm/norm-squared (vector/add left right) = norm/norm-squared left + norm/norm-squared right

norm/norm-squared-left-at-most-orthogonal-sum :
  (left right : List ℚ) (shape : vector/same-shape left right)
  (orthogonal : vector/dot left right = 0)
  → norm/norm-squared left ≤ norm/norm-squared (vector/add left right)

norm/norm-squared-right-at-most-orthogonal-sum :
  (left right : List ℚ) (shape : vector/same-shape left right)
  (orthogonal : vector/dot left right = 0)
  → norm/norm-squared right ≤ norm/norm-squared (vector/add left right)