rainbow.math.sums.equality-lp-bound

Finite sums src/rainbow/math/sums/equality_lp_bound.clj0 definitions, 1 theorems

Weak duality for equality rows and unrestricted dual prices. Reuses the existing bilinear-swap theorem; only the rival variables must be nonnegative.

Depends onmath.sums.lp-bounds math.rational.signed.multiply-associative math.linear.matrix.action-scale

signed/expr-sum-equality-lp-weak-duality

TheoremFor all inputsNo axiomsSource

signed/expr-sum-equality-lp-weak-duality :
  (A : ℕ → ℕ → ℚ) (b c x y : ℕ → ℚ) (m n : ℕ)
  (rows : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx m), signed/expr-sum-value (fun j => A idx j · x j) n = b idx)
  (xn : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ x idx)
  (dual : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), signed/expr-sum-value (fun i => A i idx · y i) m ≤ c idx)
  → signed/expr-sum-value (fun z => b z · y z) m ≤ signed/expr-sum-value (fun z => c z · x z) n

0 = signed/zero= = signed/equivalent: equality of rational values· = signed/multiplyℕ = data/Natℚ = signed/SignedRational≤ = signed/at-most