Reference · Finite types, distributions and Markov chains

rainbow.math.finite.vector

Finite types, distributions and Markov chainssrc/rainbow/math/finite/vector.clj4 definitions, 5 theorems

Finite vectors over signed rationals: lists of signed-rational components with elementwise addition, negation, subtraction, and scalar scaling. This is the first genuinely n-dimensional state in the corpus, the foundation for multi-dimensional optimization and filtering. Scaling and negation reuse the list map; elementwise addition is a zip of the two component lists via the list recursor.

vector/scale :
  (x₁ : ℚ≥0) (x₂ : List ℚ)
  → List ℚ

vector/negate :
  (x₁ : List ℚ)
  → List ℚ

vector/add :
  (x₁ x₂ : List ℚ)
  → List ℚ

vector/subtract :
  (x₁ x₂ : List ℚ)
  → List ℚ

vector/add-nil :
  (right : List ℚ)
  → vector/add [] right = []

vector/subtract-unfold :
  (left right : List ℚ)
  → vector/subtract left right = vector/add left (vector/negate right)

vector/add-example :
  → vector/add [signed/from-nnrat 1, signed/from-nnrat 2] [signed/from-nnrat 3, signed/from-nnrat 4] = [signed/from-nnrat 4, signed/from-nnrat 6]

vector/scale-example :
  → vector/scale 2 [signed/from-nnrat 1, signed/from-nnrat 2] = [signed/from-nnrat 2, signed/from-nnrat 4]

vector/add-example-3d :
  → vector/add [signed/from-nnrat 1, signed/from-nnrat 2, signed/from-nnrat 3] [signed/from-nnrat 3, signed/from-nnrat 4, signed/from-nnrat 5] = [signed/from-nnrat 4, signed/from-nnrat 6, signed/from-nnrat 8]