Reference · Algorithm guarantees

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

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

Finite normalized consensus trajectories remain inside invariant intervals.

Depends onalgorithms.proofs.particle-swarm-convex-move

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

swarm/nnrat-convex-trajectory-zero :
  (w-position w-best : ℚ≥0) (bests : ℕ → List ℚ) (initial : List ℚ)
  → swarm/nnrat-convex-trajectory w-position w-best bests initial 0 = initial

swarm/nnrat-convex-trajectory-successor :
  (w-position w-best : ℚ≥0) (bests : ℕ → List ℚ) (initial : List ℚ) (steps : ℕ)
  → swarm/nnrat-convex-trajectory w-position w-best bests initial (data/succ steps) = swarm/nnrat-convex-move w-position w-best (trajectory) (bests steps)
  where trajectory := swarm/nnrat-convex-trajectory w-position w-best bests initial steps

swarm/nnrat-convex-trajectory-lower-bound :
  (w-position w-best : ℚ≥0) (bests : ℕ → List ℚ) (initial lower : List ℚ)
  (normalized : w-position + w-best = 1)
  (initial-lower : vector/at-most lower initial)
  (best-lower : ∀ (step : ℕ), vector/at-most lower (bests step)) (steps : ℕ)
  → (fun steps₁ => vector/at-most lower (swarm/nnrat-convex-trajectory w-position w-best bests initial steps₁)) steps

swarm/nnrat-convex-trajectory-upper-bound :
  (w-position w-best : ℚ≥0) (bests : ℕ → List ℚ) (initial upper : List ℚ)
  (normalized : w-position + w-best = 1)
  (initial-upper : vector/at-most initial upper)
  (best-upper : ∀ (step : ℕ), vector/at-most (bests step) upper) (steps : ℕ)
  → (fun steps₁ => vector/at-most (swarm/nnrat-convex-trajectory w-position w-best bests initial steps₁) upper) steps

swarm/nnrat-convex-trajectory-in-interval :
  (w-position w-best : ℚ≥0) (bests : ℕ → List ℚ) (initial lower upper : List ℚ)
  (normalized : w-position + w-best = 1)
  (initial-lower : vector/at-most lower initial)
  (initial-upper : vector/at-most initial upper)
  (best-lower : ∀ (step : ℕ), vector/at-most lower (bests step))
  (best-upper : ∀ (step : ℕ), vector/at-most (bests step) upper) (steps : ℕ)
  → proposition/conjunction (most) (most₁)
  where most := vector/at-most lower (swarm/nnrat-convex-trajectory w-position w-best bests initial steps)
  where most₁ := vector/at-most (swarm/nnrat-convex-trajectory w-position w-best bests initial steps) upper