Reference · Algorithm guarantees

rainbow.algorithms.proofs.particle-swarm-global-best

Algorithm guarantees src/rainbow/algorithms/proofs/particle_swarm_global_best.clj2 definitions, 7 theorems

Verified finite-swarm global-best selection and best-so-far monotonicity.

swarm/nnrat-global-best

swarm/nnrat-global-best :
  (x₁ : List ℚ → ℚ≥0) (x₂ : Finset (List ℚ)) (x₃ : List ℚ)
  → List ℚ

Finset = finset-data/FinsetList = data/Listℚ = signed/SignedRationalℚ≥0 = nnrat/NonnegativeRational

swarm/nnrat-best-so-far

DefinitionSource, line 65

swarm/nnrat-best-so-far :
  (x₁ : List ℚ → ℚ≥0) (x₂ x₃ : List ℚ)
  → List ℚ

List = data/Listℚ = signed/SignedRationalℚ≥0 = nnrat/NonnegativeRational

swarm/nnrat-global-best-unfold

TheoremHolds by unfolding a definitionNo axiomsSource, line 80

swarm/nnrat-global-best-unfold :
  (objective : List ℚ → ℚ≥0) (positions : Finset (List ℚ)) (initial : List ℚ)
  → swarm/nnrat-global-best objective positions initial = decision/finite-nnrat-argmin (List ℚ) positions initial objective

= = equality/EqFinset = finset-data/FinsetList = data/Listℚ = signed/SignedRationalℚ≥0 = nnrat/NonnegativeRational

swarm/nnrat-global-best-is-member

TheoremFor all inputsNo axiomsSource, line 101

swarm/nnrat-global-best-is-member :
  (objective : List ℚ → ℚ≥0) (positions : Finset (List ℚ)) (initial : List ℚ)
  (initial-member : initial ∈ positions)
  → swarm/nnrat-global-best objective positions initial ∈ positions

Finset = finset-data/FinsetList = data/Listℚ = signed/SignedRationalℚ≥0 = nnrat/NonnegativeRational∈ = finset-data/to-set: membership in a finite set

swarm/nnrat-global-best-dominates

TheoremFor all inputsNo axiomsSource, line 124

swarm/nnrat-global-best-dominates :
  (objective : List ℚ → ℚ≥0) (positions : Finset (List ℚ)) (initial candidate : List ℚ)
  (candidate-member : candidate ∈ positions)
  → objective (swarm/nnrat-global-best objective positions initial) ≤ objective candidate

Finset = finset-data/FinsetList = data/Listℚ = signed/SignedRationalℚ≥0 = nnrat/NonnegativeRational∈ = finset-data/to-set: membership in a finite set≤ = nnrat/at-most

swarm/nnrat-best-so-far-unfold

TheoremHolds by unfolding a definitionNo axiomsSource, line 150

swarm/nnrat-best-so-far-unfold :
  (objective : List ℚ → ℚ≥0) (previous candidate : List ℚ)
  → swarm/nnrat-best-so-far objective previous candidate = decision/nnrat-select-min (List ℚ) objective previous candidate

= = equality/EqList = data/Listℚ = signed/SignedRationalℚ≥0 = nnrat/NonnegativeRational

swarm/nnrat-best-so-far-is-previous-or-candidate

TheoremFor all inputsNo axiomsSource, line 171

swarm/nnrat-best-so-far-is-previous-or-candidate :
  (objective : List ℚ → ℚ≥0) (previous candidate : List ℚ)
  → proposition/disjunction (far = previous) (far = candidate)
  where far := swarm/nnrat-best-so-far objective previous candidate

= = equality/EqList = data/Listℚ = signed/SignedRationalℚ≥0 = nnrat/NonnegativeRational

swarm/nnrat-best-so-far-bounds-previous

TheoremFor all inputsNo axiomsSource, line 193

swarm/nnrat-best-so-far-bounds-previous :
  (objective : List ℚ → ℚ≥0) (previous candidate : List ℚ)
  → objective (swarm/nnrat-best-so-far objective previous candidate) ≤ objective previous

List = data/Listℚ = signed/SignedRationalℚ≥0 = nnrat/NonnegativeRational≤ = nnrat/at-most

swarm/nnrat-best-so-far-bounds-candidate

TheoremFor all inputsNo axiomsSource, line 213

swarm/nnrat-best-so-far-bounds-candidate :
  (objective : List ℚ → ℚ≥0) (previous candidate : List ℚ)
  → objective (swarm/nnrat-best-so-far objective previous candidate) ≤ objective candidate

List = data/Listℚ = signed/SignedRationalℚ≥0 = nnrat/NonnegativeRational≤ = nnrat/at-most