Reference · Signed rationals

rainbow.math.rational.signed.lp-duality

Signed rationalssrc/rainbow/math/rational/signed/lp_duality.clj0 definitions, 3 theorems

Linear-programming weak duality and the optimality certificate over SIGNED rationals -- arbitrary matrix, costs and right-hand side, any of them negative. For the program maximize c . x subject to (M x)_i <= b_i for every row i, x >= 0 and a dual-feasible y >= 0 with c_j <= (M^T y)_j for every column j, optimization/signed-lp-weak-duality : c . x <= b . y and, when a primal/dual pair closes the gap, optimization/signed-lp-optimality-certificate : b . y ~ c . x -> c . x' <= c . x for every feasible x' so the pair is a machine-checkable proof that x is optimal, with no need to trust the solver that produced it. The existing nnrat LP stack proves the same statements only for NONNEGATIVE data, which excludes most real programs (costs to minimize, equality constraints split into two inequalities, any variable with a negative coefficient). This is the general form. The argument is double counting on the term family T i j = (M i j * x j) * y i whose row totals are bounded by the primal constraints and whose column totals bound the dual objective: ROW sum_j T i j ~ (M x)_i * y_i <= b_i * y_i [scale-right, then multiply-right-monotone against y_i >= 0] COLUMN c_j * x_j <= (M^T y)_j * x_j ~ sum_i (M i j * y i) * x j ~ sum_i (M i j * x j) * y i = sum_i T i j and `optimization/signed-double-counting-weak-duality` closes it with Fubini. The last step of the column bound is `signed/multiply-swap-outer`, which only became available with the nnrat-ring tactic. Native and axiom-free; chains the signed Fubini and associativity modules on D63.

Depends onmath.rational.signed.fubinimath.rational.signed.multiply-associative

optimization/signed-lp-column-bound.{u} :
  (A : Type u) (coeff weights : A → ℚ) (scalar cost : ℚ) (is : List A)
  (dual-feasible : cost ≤ Σ i∈is, coeff i · weights i)
  (nonnegative : 0 ≤ scalar)
  → cost · scalar ≤ Σ i∈is, coeff i · scalar · weights i

optimization/signed-lp-weak-duality.{u} :
  (A B : Type u) (M : A → B → ℚ) (b : A → ℚ) (c x : B → ℚ) (y : A → ℚ) (rows : List A)
  (cols : List B)
  (primal-feasible : ∀ (i : A), Σ j∈cols, M i j · x j ≤ b i)
  (dual-feasible : ∀ (j : B), c j ≤ Σ i∈rows, M i j · y i)
  (x-nonnegative : ∀ (j : B), 0 ≤ x j)
  (y-nonnegative : ∀ (i : A), 0 ≤ y i)
  → Σ j∈cols, c j · x j ≤ Σ i∈rows, b i · y i

optimization/signed-lp-optimality-certificate.{u} :
  (A B : Type u) (M : A → B → ℚ) (b : A → ℚ) (c x : B → ℚ) (y : A → ℚ) (rows : List A)
  (cols : List B)
  (primal-feasible : ∀ (i : A), Σ j∈cols, M i j · x j ≤ b i)
  (dual-feasible : ∀ (j : B), c j ≤ Σ i∈rows, M i j · y i)
  (x-nonnegative : ∀ (j : B), 0 ≤ x j)
  (y-nonnegative : ∀ (i : A), 0 ≤ y i)
  (gap : Σ i∈rows, b i · y i = Σ j∈cols, c j · x j)
  (candidate : B → ℚ)
  (candidate-feasible : ∀ (i : A), Σ j∈cols, M i j · candidate j ≤ b i)
  (candidate-nonnegative : ∀ (j : B), 0 ≤ candidate j)
  → Σ j∈cols, c j · candidate j ≤ Σ j∈cols, c j · x j