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

Reference · Finite sums

rainbow.math.sums.lp-two-blocks

Finite sumssrc/rainbow/math/sums/lp_two_blocks.clj0 definitions, 1 theorems

Weak duality with two separate constraint blocks, by two applications of the existing LP theorem. No interpretation of either block is assumed.

Depends onmath.sums.lp-boundsmath.rational.signed.order-monotone

signed/expr-sum-lp-two-block-weak-duality

TheoremFor all inputsNo axiomsSource

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

+ = signed/add0 = signed/zero· = signed/multiplyℕ = data/Natℚ = signed/SignedRational≤ = signed/at-most