Reference · Vectors

rainbow.math.linear.vector.uniform-clamp

Vectorssrc/rainbow/math/linear/vector/uniform_clamp.clj2 definitions, 6 theorems

Uniform box projection for finite signed-rational vectors. vector/uniform-clamp lower upper values = map (signed/clamp lower upper) values `vector/in-band` is proof data asserting that every component lies between the same lower and upper bounds. Projection produces that evidence for every ordered interval, respects length-sensitive componentwise vector equivalence, and is idempotent up to vector equivalence. This lifts the scalar signed lattice into the n-dimensional representation already used by Rainbow's optimization algorithms. It is the reusable core of uniform box constraints and projected first-order methods. Native and axiom-free on D63.

Depends onmath.rational.signed.clampmath.linear.vector.equivalence

vector/uniform-clamp :
  (x₁ x₂ : ℚ) (x₃ : List ℚ)
  → List ℚ

vector/in-band :
  (x₁ x₂ : ℚ) (x₃ : List ℚ)
  → Prop

vector/in-band-empty :
  (lower upper : ℚ)
  → vector/in-band lower upper []

vector/in-band-cons :
  (lower upper head : ℚ) (tail : List ℚ)
  (above-lower : lower ≤ head)
  (below-upper : head ≤ upper)
  (tail-in-band : vector/in-band lower upper tail)
  → vector/in-band lower upper (data/cons ℚ head tail)

vector/uniform-clamp-in-band :
  (lower upper : ℚ)
  (ordered : lower ≤ upper)
  (values : List ℚ)
  → vector/in-band lower upper (vector/uniform-clamp lower upper values)

vector/uniform-clamp-respects-equivalence :
  (lower upper : ℚ) (left right : List ℚ) (same : vector/equivalent left right)
  → vector/equivalent (vector/uniform-clamp lower upper left) (vector/uniform-clamp lower upper right)

vector/uniform-clamp-preserves-in-band :
  (lower upper : ℚ) (values : List ℚ) (bounded : vector/in-band lower upper values)
  → vector/equivalent (vector/uniform-clamp lower upper values) values

vector/uniform-clamp-idempotent :
  (lower upper : ℚ)
  (ordered : lower ≤ upper)
  (values : List ℚ)
  → vector/equivalent (clamp) (vector/uniform-clamp lower upper values)
  where clamp := vector/uniform-clamp lower upper (vector/uniform-clamp lower upper values)