Reference · Algorithm guarantees

rainbow.algorithms.proofs.admm

Algorithm guaranteessrc/rainbow/algorithms/proofs/admm.clj1 definitions, 3 theorems

AHoF O51 ADMM (Alternating Direction Method of Multipliers): the scaled-form dual variable update over vector-valued state. After the x- and z-subproblems, the scaled dual variable accumulates the primal residual x - z: u' = u + (x - z) Every term is a finite-vector operation (subtract, add), reusing the shared n-dimensional vector state. The x-update argmin_x ( f(x) + (rho/2)||x - z + u||^2 ) and the z-update are problem-specific minimizations supplied to the loop (not exact-rational in general and executable-only); what is proved here is the deterministic scaled dual recurrence and worked instances from a zero- initialized dual variable, where the residual passes through by reflexivity. Scope (measured by the kernel): this module has 2 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.admm` prints this classification.

Depends onmath.finite.vector

admm/dual-update :
  (x₁ x₂ x₃ : List ℚ)
  → List ℚ

admm/dual-update-unfold :
  (dual x z : List ℚ)
  → admm/dual-update dual x z = vector/add dual (vector/subtract x z)

admm/residual-2d-example :
  → admm/dual-update [signed/from-nnrat 0, signed/from-nnrat 0] [signed/from-nnrat 3, signed/from-nnrat 2] [signed/from-nnrat 0, signed/from-nnrat 0] = [signed/from-nnrat 3, signed/from-nnrat 2]

admm/residual-3d-example :
  → admm/dual-update [signed/from-nnrat 0, signed/from-nnrat 0, signed/from-nnrat 0] [signed/from-nnrat 2, signed/from-nnrat 4, signed/from-nnrat 6] [signed/from-nnrat 0, signed/from-nnrat 0, signed/from-nnrat 0] = [signed/from-nnrat 2, signed/from-nnrat 4, signed/from-nnrat 6]