Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.mccormick-sandwich

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

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

signed/mccormick-under

TheoremFor all inputsNo axiomsSource

signed/mccormick-under :
  (mu-a mu-b mu-x mu-y : ℚ)
  (mu-h : 0 ≤ (mu-x + signed/negate mu-a) · (mu-y + signed/negate mu-b))
  → mu-a · mu-y + mu-x · mu-b + signed/negate (mu-a · mu-b) ≤ mu-x · mu-y

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

signed/mccormick-over

TheoremFor all inputsNo axiomsSource

signed/mccormick-over :
  (mo-a mo-b mo-x mo-y : ℚ)
  (mo-h : 0 ≤ (mo-a + signed/negate mo-x) · (mo-y + signed/negate mo-b))
  → mo-x · mo-y ≤ mo-a · mo-y + mo-x · mo-b + signed/negate (mo-a · mo-b)

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

signed/mccormick-coordinate

TheoremFor all inputsNo axiomsSource

signed/mccormick-coordinate :
  (mt-x mt-y mt-xl mt-xu mt-yl mt-yu mt-lo mt-hi : ℚ)
  (mt-g0 : mt-xl ≤ mt-x)
  (mt-g1 : mt-x ≤ mt-xu)
  (mt-g2 : mt-yl ≤ mt-y)
  (mt-g3 : mt-y ≤ mt-yu)
  (mt-g4 : mt-xl · mt-y + mt-x · mt-yl + signed/negate (mt-xl · mt-yl) ≤ mt-lo)
  (mt-g5 : mt-xu · mt-y + mt-x · mt-yu + signed/negate (mt-xu · mt-yu) ≤ mt-lo)
  (mt-g6 : (mt-lo + signed/negate (mt-xl · mt-y + mt-x · mt-yl + signed/negate (mt-xl · mt-yl))) · (mt-lo + signed/negate (mt-xu · mt-y + mt-x · mt-yu + signed/negate (mt-xu · mt-yu))) = 0)
  (mt-g8 : mt-hi ≤ mt-xu · mt-y + mt-x · mt-yl + signed/negate (mt-xu · mt-yl))
  (mt-g9 : mt-hi ≤ mt-xl · mt-y + mt-x · mt-yu + signed/negate (mt-xl · mt-yu))
  (mt-g10 : (mt-xu · mt-y + mt-x · mt-yl + signed/negate (mt-xu · mt-yl) + signed/negate mt-hi) · (mt-xl · mt-y + mt-x · mt-yu + signed/negate (mt-xl · mt-yu) + signed/negate mt-hi) = 0)
  → proposition/conjunction (conjunction₁) (conjunction)
  where conjunction := proposition/conjunction (proposition/conjunction (proposition/disjunction (mt-hi = mt-xu · mt-y + mt-x · mt-yl + signed/negate (mt-xu · mt-yl)) (mt-hi = mt-xl · mt-y + mt-x · mt-yu + signed/negate (mt-xl · mt-yu))) (proposition/conjunction (mt-hi ≤ mt-xu · mt-y + mt-x · mt-yl + signed/negate (mt-xu · mt-yl)) (mt-hi ≤ mt-xl · mt-y + mt-x · mt-yu + signed/negate (mt-xl · mt-yu)))) (proposition/conjunction (mt-lo ≤ mt-x · mt-y) (mt-x · mt-y ≤ mt-hi))
  where conjunction₁ := proposition/conjunction (proposition/disjunction (mt-lo = mt-xl · mt-y + mt-x · mt-yl + signed/negate (mt-xl · mt-yl)) (mt-lo = mt-xu · mt-y + mt-x · mt-yu + signed/negate (mt-xu · mt-yu))) (proposition/conjunction (mt-xl · mt-y + mt-x · mt-yl + signed/negate (mt-xl · mt-yl) ≤ mt-lo) (mt-xu · mt-y + mt-x · mt-yu + signed/negate (mt-xu · mt-yu) ≤ mt-lo))

+ = signed/add0 = signed/zero= = signed/equivalent: equality of rational values· = signed/multiplyℚ = signed/SignedRational≤ = signed/at-most