Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.kkt

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/kkt.clj1 definitions, 3 theorems

AHoF O53 Lagrange Multipliers (KKT): the stationarity condition of the Karush-Kuhn-Tucker system. Reformulating a constrained problem as a system of equations, the Lagrangian gradient must vanish; for a single equality constraint the stationarity residual is stationarity gradF lambda gradG = gradF + lambda * gradG over the finite-vector state, and a KKT point is a (x, lambda) where this residual is the zero vector. Every term is an exact finite-vector operation (scale, add), reusing the shared n-dimensional vector state. The gradients gradF, gradG and the multiplier lambda are problem data (differentiation and the root solve are executable / not exact-rational in general); what is proved here is the deterministic stationarity combination and a worked instance where a zero objective gradient makes the residual land exactly on lambda * gradG. 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.ahof.kkt` prints this classification.

Depends onmath.finite.vector

kkt/stationarity :
  (x₁ : List ℚ) (x₂ : ℚ≥0) (x₃ : List ℚ)
  → List ℚ

kkt/stationarity-unfold :
  (grad-f : List ℚ) (lambda : ℚ≥0) (grad-g : List ℚ)
  → hmc/drift grad-f lambda grad-g = vector/add grad-f (vector/scale lambda grad-g)

kkt/stationarity-example :
  → hmc/drift [signed/from-nnrat 0, signed/from-nnrat 0] 1 [signed/from-nnrat 3, signed/from-nnrat 2] = [signed/from-nnrat 3, signed/from-nnrat 2]

kkt/stationarity-3d-example :
  → hmc/drift [signed/from-nnrat 0, signed/from-nnrat 0, signed/from-nnrat 0] 1 [signed/from-nnrat 2, signed/from-nnrat 4, signed/from-nnrat 6] = [signed/from-nnrat 2, signed/from-nnrat 4, signed/from-nnrat 6]