Reference · Finite sums

rainbow.math.sums.lp-mixed-bound

Finite sumssrc/rainbow/math/sums/lp_mixed_bound.clj0 definitions, 4 theorems

A free-price equality block, nonnegative-price upper rows and unit upper bounds. Reuses equality LP and inequality LP weak duality; all rival premises are explicit.

Depends onmath.sums.equality-lp-boundmath.rational.signed.order-monotone

signed/expr-sum-lp-mixed-upper-penalty-bound :
  (A : ℕ → ℕ → ℚ) (b : ℕ → ℚ) (C : ℕ → ℕ → ℚ) (d c x y u w : ℕ → ℚ) (m p n : ℕ)
  (rows : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx m), signed/expr-sum-value (fun j => A idx j · x j) n = b idx)
  (cuts : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx p), signed/expr-sum-value (fun j => C idx j · x j) n ≤ d idx)
  (xn : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ x idx)
  (unit : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), x idx ≤ 1)
  (un : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx p), 0 ≤ u idx)
  (wn : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ w idx)
  (dual : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), signed/expr-sum-value (fun i => A i idx · y i) m ≤ (fun column => c column + signed/expr-sum-value (fun i => C i column · u i) p + w column) idx)
  → signed/expr-sum-value (fun z => b z · y z) m ≤ signed/expr-sum-value (fun z => c z · x z) n + signed/expr-sum-value (fun z => d z · u z) p + signed/expr-sum-value w n

signed/cancel-shared-addend-bound :
  (x y common : ℚ)
  (bound : x + common ≤ y + common)
  → x ≤ y

signed/unit-penalty-product :
  (size price : ℚ)
  → (size + signed/negate 1) · price = size · price + signed/negate price

signed/restore-subtracted-penalty :
  (cost sizes prices box : ℚ)
  → cost + (sizes + signed/negate prices) + box + prices = cost + sizes + box