Reference · Vectors

rainbow.math.linear.vector.projected-gradient

Vectorssrc/rainbow/math/linear/vector/projected_gradient.clj1 definitions, 4 theorems

Projected-gradient steps on finite signed-rational vectors. projected-step lo hi rate point gradient = uniform-clamp lo hi (point - rate * gradient) This composes Rainbow's native vector arithmetic with the signed box projection. Every step is componentwise feasible for an ordered interval; projecting it again is idempotent up to vector equivalence; and projection preserves any componentwise order already established between two raw updates. These are n-dimensional theorems, not scalar projection aliases. Native and axiom-free on D63.

Depends onmath.finite.vectormath.linear.vector.pointwise-order-laws

optimization/vector-projected-step :
  (x₁ x₂ : ℚ) (x₃ : ℚ≥0) (x₄ x₅ : List ℚ)
  → List ℚ

optimization/vector-projected-step-unfold :
  (lower upper : ℚ) (rate : ℚ≥0) (point gradient : List ℚ)
  → optimization/vector-projected-step lower upper rate point gradient = vector/uniform-clamp lower upper (subtract)
  where subtract := vector/subtract point (vector/scale rate gradient)

optimization/vector-projected-step-in-band :
  (lower upper : ℚ)
  (ordered : lower ≤ upper)
  (rate : ℚ≥0) (point gradient : List ℚ)
  → vector/in-band lower upper (step)
  where step := optimization/vector-projected-step lower upper rate point gradient

optimization/vector-projected-step-reprojection :
  (lower upper : ℚ)
  (ordered : lower ≤ upper)
  (rate : ℚ≥0) (point gradient : List ℚ)
  → vector/equivalent (clamp) (optimization/vector-projected-step lower upper rate point gradient)
  where clamp := vector/uniform-clamp lower upper (optimization/vector-projected-step lower upper rate point gradient)

optimization/vector-projected-step-monotone :
  (lower upper : ℚ) (rate : ℚ≥0)
  (left-point left-gradient right-point right-gradient : List ℚ)
  (raw-ordered : vector/at-most (subtract₃) (subtract))
  → vector/at-most (step₁) (step)
  where step := optimization/vector-projected-step lower upper rate right-point right-gradient
  where step₁ := optimization/vector-projected-step lower upper rate left-point left-gradient
  where subtract := vector/subtract right-point (vector/scale rate right-gradient)
  where subtract₃ := vector/subtract left-point (vector/scale rate left-gradient)