Reference · Algorithm guarantees

rainbow.algorithms.proofs.particle-swarm-projected-trajectory

Algorithm guaranteessrc/rainbow/algorithms/proofs/particle_swarm_projected_trajectory.clj2 definitions, 6 theorems

Box-projected particle updates and finite-horizon trajectory boundedness.

Depends onmath.finite.vectoralgorithms.proofs.particle-swarmmath.linear.vector.uniform-clamp

swarm/projected-step :
  (x₁ x₂ : ℚ) (x₃ x₄ x₅ : ℚ≥0) (x₆ x₇ x₈ x₉ : List ℚ)
  → List ℚ

swarm/projected-trajectory :
  (x₁ x₂ : ℚ) (x₃ : ℕ → List ℚ → List ℚ) (x₄ : List ℚ) (x₅ : ℕ)
  → List ℚ

swarm/projected-step-unfold :
  (lower upper : ℚ) (w c1 c2 : ℚ≥0) (velocity position pbest gbest : List ℚ)
  → swarm/projected-step lower upper w c1 c2 velocity position pbest gbest = vector/uniform-clamp lower upper (step)
  where step := swarm/step w c1 c2 velocity position pbest gbest

swarm/projected-step-in-band :
  (lower upper : ℚ)
  (ordered : lower ≤ upper)
  (w c1 c2 : ℚ≥0) (velocity position pbest gbest : List ℚ)
  → vector/in-band lower upper (step)
  where step := swarm/projected-step lower upper w c1 c2 velocity position pbest gbest

swarm/projected-trajectory-zero :
  (lower upper : ℚ) (update : ℕ → List ℚ → List ℚ) (initial : List ℚ)
  → swarm/projected-trajectory lower upper update initial 0 = initial

swarm/projected-trajectory-successor :
  (lower upper : ℚ) (update : ℕ → List ℚ → List ℚ) (initial : List ℚ) (steps : ℕ)
  → swarm/projected-trajectory lower upper update initial (data/succ steps) = vector/uniform-clamp lower upper (update steps (trajectory))
  where trajectory := swarm/projected-trajectory lower upper update initial steps

swarm/projected-trajectory-successor-in-band :
  (lower upper : ℚ)
  (ordered : lower ≤ upper)
  (update : ℕ → List ℚ → List ℚ) (initial : List ℚ) (steps : ℕ)
  → vector/in-band lower upper (trajectory)
  where trajectory := swarm/projected-trajectory lower upper update initial (data/succ steps)

swarm/projected-trajectory-in-band :
  (lower upper : ℚ)
  (ordered : lower ≤ upper)
  (update : ℕ → List ℚ → List ℚ) (initial : List ℚ)
  (initial-in-band : vector/in-band lower upper initial) (steps : ℕ)
  → (fun steps₁ => vector/in-band lower upper (swarm/projected-trajectory lower upper update initial steps₁)) steps