rainbow.math.lemmas.lp-duality

Lemmas behind operations-research checks src/rainbow/math/lemmas/lp_duality.clj0 definitions, 1 theorems

General lemmas: lp duality. The mathematical facts the corresponding checks rest on, each checked by the kernel.

signed/expr-sum-lp-weak-duality

TheoremFor all inputsNo axiomsSource

signed/expr-sum-lp-weak-duality :
  (A : ℕ → ℕ → ℚ) (b c x y : ℕ → ℚ) (m n : ℕ)
  (primal : ∀ (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)
  (yn : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx m), 0 ≤ y 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 z => c z · x z) n ≤ signed/expr-sum-value (fun z => b z · y z) m

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