Reference · Vectors

rainbow.math.linear.vector.norm-expansion

Vectorssrc/rainbow/math/linear/vector/norm_expansion.clj0 definitions, 2 theorems

Exact quadratic expansions for the native signed squared norm. norm/norm-squared-add norm/norm-squared-subtract For same-shaped vectors, squared norm expands into the four expected dot terms. The subtraction law retains nested signed subtraction, which is the exact Grothendieck-pair form of a^2 - a*b - b*a + b^2. Both results are theorem-only compositions of dot additivity/subtractivity.

Depends onmath.linear.vector.dot-subtractmath.linear.vector.norm

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

norm/norm-squared-subtract :
  (left right : List ℚ) (same : vector/same-shape left right)
  → norm/norm-squared (vector/subtract left right) = norm/norm-squared left - vector/dot left right - (vector/dot right left - norm/norm-squared right)