Reference · Algorithm guarantees

rainbow.algorithms.proofs.particle-swarm-convex-move

Algorithm guaranteessrc/rainbow/algorithms/proofs/particle_swarm_convex_move.clj1 definitions, 5 theorems

Normalized movement toward a swarm best preserves vector intervals.

Depends onmath.linear.vector.convex-combination

swarm/nnrat-convex-move :
  (x₁ x₂ : ℚ≥0) (x₃ x₄ : List ℚ)
  → List ℚ

swarm/nnrat-convex-move-unfold :
  (w-position w-best : ℚ≥0) (position best : List ℚ)
  → swarm/nnrat-convex-move w-position w-best position best = vector/nnrat-wsum2 w-position w-best position best

swarm/nnrat-convex-move-lower-bound :
  (w-position w-best : ℚ≥0) (position best lower : List ℚ)
  (normalized : w-position + w-best = 1)
  (lower-position : vector/at-most lower position)
  (lower-best : vector/at-most lower best)
  → vector/at-most lower (move)
  where move := swarm/nnrat-convex-move w-position w-best position best

swarm/nnrat-convex-move-upper-bound :
  (w-position w-best : ℚ≥0) (position best upper : List ℚ)
  (normalized : w-position + w-best = 1)
  (position-upper : vector/at-most position upper)
  (best-upper : vector/at-most best upper)
  → vector/at-most (move) upper
  where move := swarm/nnrat-convex-move w-position w-best position best

swarm/nnrat-convex-move-between-position-and-best :
  (w-position w-best : ℚ≥0) (position best : List ℚ)
  (normalized : w-position + w-best = 1)
  (ordered : vector/at-most position best)
  → proposition/conjunction (most) (most₁)
  where most := vector/at-most position (swarm/nnrat-convex-move w-position w-best position best)
  where most₁ := vector/at-most (swarm/nnrat-convex-move w-position w-best position best) best

swarm/nnrat-convex-move-between-best-and-position :
  (w-position w-best : ℚ≥0) (position best : List ℚ)
  (normalized : w-position + w-best = 1)
  (ordered : vector/at-most best position)
  → proposition/conjunction (most₁) (most)
  where most := vector/at-most (swarm/nnrat-convex-move w-position w-best position best) position
  where most₁ := vector/at-most best (swarm/nnrat-convex-move w-position w-best position best)