Reference · Vectors

rainbow.math.linear.vector.norm

Vectors src/rainbow/math/linear/vector/norm.clj2 definitions, 3 theorems

The Euclidean vector norm over signed-rational vectors, built from the inner product and the perfect-square root witness: norm-squared v = <v, v> is-norm v n <=> n * n ~ <v, v> The squared norm is exact (a dot product); the norm itself is exact only on perfect-square instances (a witness n with n*n ~ norm-squared). Worked: [3,4] has squared norm 25 and norm 5. This unblocks gradient-norm stopping criteria, vector normalization, and cosine similarity. Requires `signed/multiply` and `vector/dot` in the environment.

norm/norm-squared

DefinitionSource, line 68

norm/norm-squared :
  (x₁ : List ℚ)
  → ℚ

List = data/Listℚ = signed/SignedRational

norm/is-norm

DefinitionSource, line 73

norm/is-norm :
  (x₁ : List ℚ) (x₂ : ℚ)
  → Prop

List = data/Listℚ = signed/SignedRational

norm/norm-squared-example

TheoremWorked exampleNo axiomsSource, line 85

norm/norm-squared-example :
  → norm/norm-squared [signed/from-nnrat 3, signed/from-nnrat 4] = signed/from-nnrat 25

= = signed/equivalent: equality of rational values

norm/norm-example

TheoremWorked exampleNo axiomsSource, line 95

norm/norm-example :
  → norm/is-norm [signed/from-nnrat 3, signed/from-nnrat 4] (signed/from-nnrat 5)

norm/unit-norm-example

TheoremWorked exampleNo axiomsSource, line 104

norm/unit-norm-example :
  → norm/is-norm [signed/from-nnrat 1, signed/from-nnrat 0, signed/from-nnrat 0] (signed/from-nnrat 1)