Reference · Algorithm guarantees

rainbow.algorithms.proofs.nelder-mead

Algorithm guaranteessrc/rainbow/algorithms/proofs/nelder_mead.clj1 definitions, 2 theorems

AHoF O36 Nelder-Mead Simplex: the reflection move, the workhorse simplex transform. The worst vertex is reflected through the centroid of the remaining vertices: reflected = centroid + (centroid - worst) a finite-vector subtract and add (unit reflection coefficient). Because the reflection subtracts a non-origin vertex, its components come out as non-canonical Grothendieck pairs, so the worked result is proven with the componentwise vector equivalence (vector/equivalent) rather than pair equality -- the first optimizer worked example away from the origin. The expand, contract, and shrink moves and the centroid computation stay in the executable reference. Requires the finite-vector and vector-equivalence capabilities. Scope (measured by the kernel): this module has 1 worked instances (statements about specific values) and 1 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.nelder-mead` prints this classification.

Depends onmath.linear.vector.equivalencemath.finite.vector

nelder/reflect :
  (x₁ x₂ : List ℚ)
  → List ℚ

nelder/reflect-unfold :
  (centroid worst : List ℚ)
  → nelder/reflect centroid worst = vector/add centroid (vector/subtract centroid worst)

nelder/reflect-example :
  → vector/equivalent (reflect) [signed/from-nnrat 3, signed/from-nnrat 3]
  where reflect := nelder/reflect [signed/from-nnrat 2, signed/from-nnrat 2] [signed/from-nnrat 1, signed/from-nnrat 1]