Reference · Vectors

rainbow.math.linear.vector.norm-parallelogram

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

The exact parallelogram identity for native signed vectors. signed/parallelogram-recombine norm/norm-squared-parallelogram The scalar lemma cancels the two cross terms in the addition and subtraction expansions as a Grothendieck-pair semiring identity. Substituting the native squared-norm expansions yields ||a+b||^2 + ||a-b||^2 ~ (||a||^2+||a||^2) + (||b||^2+||b||^2) for same-shaped vectors, without division, square roots, or axioms.

Depends onmath.linear.vector.norm-expansion

signed/parallelogram-recombine :
  (a b c d : ℚ)
  → a + b + (c + d) + (a - b - (c - d)) = a + a + (d + d)

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