Reference · Algorithm guarantees

rainbow.algorithms.proofs.augmented-lagrangian

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

AHoF O49 Augmented Lagrangian: the dual multiplier update in the outer loop. Where the penalty method (O48) only grows a penalty weight, the augmented Lagrangian also maintains a Lagrange multiplier that is updated from the measured constraint violation each outer iteration: multiplier' = multiplier + rho * constraint a signed update (the multiplier and the constraint value may be negative). This reuses signed scaling and addition. The inner penalized minimization and the augmented-Lagrangian value itself are the executable concern; what is proved is the multiplier-update recurrence and worked instances -- a positive violation raises the multiplier, an over-satisfied constraint lowers it. 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.augmented-lagrangian` prints this classification.

lagrangian/update-multiplier :
  (x₁ : ℚ) (x₂ : ℚ≥0) (x₃ : ℚ)
  → ℚ

lagrangian/update-multiplier-unfold :
  (multiplier : ℚ) (rho : ℚ≥0) (constraint : ℚ)
  → lagrangian/update-multiplier multiplier rho constraint = multiplier + signed/scale rho constraint

lagrangian/violation-raises-example :
  → lagrangian/update-multiplier (signed/from-nnrat 1) 2 (signed/from-nnrat 1) = signed/from-nnrat 3

lagrangian/over-satisfied-example :
  → lagrangian/update-multiplier (signed/from-nnrat 3) 1 -1 = signed/from-nnrat 2