Skip to content
Flexiana
Menu
Solutions
How we work
Research
Work
Products
Company
Bring us a hard problem
Rainbow docs menu

Reference · Signed rationals

rainbow.math.rational.signed.matrix-lp-duality

Signed rationalssrc/rainbow/math/rational/signed/matrix_lp_duality.clj0 definitions, 1 theorems

Signed LP weak duality over native finite matrices and vectors. This theorem connects the LP certificate cone to matrix/vector-multiply and matrix/transpose. It is Level-3 mathematical infrastructure: it verifies the bound under explicit feasibility, nonnegativity, and shape assumptions; it does not connect a Clojure LP implementation to those assumptions.

Depends onmath.linear.matrix.action-associativemath.linear.matrix.positive-action

optimization/signed-matrix-lp-weak-duality

TheoremFor all inputsNo axiomsSource, line 59

optimization/signed-matrix-lp-weak-duality :
  (rows : List (List ℚ)) (b c x y : List ℚ)
  (y-row-shape : vector/same-shape y (matrix/column-shape rows))
  (rows-x-compatible : matrix/compatible rows x)
  (primal-feasible : vector/at-most (matrix/vector-multiply rows x) b)
  (dual-feasible : vector/at-most c (multiply))
  (x-nonnegative : vector/at-most (vector/zero-like x) x)
  (y-nonnegative : vector/at-most (vector/zero-like y) y)
  → vector/dot c x ≤ vector/dot b y
  where multiply := matrix/vector-multiply (matrix/transpose rows) y

List = data/Listℚ = signed/SignedRational≤ = signed/at-most