rainbow.math.lemmas.bin-packing-bound

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

General lemmas: bin packing bound. The mathematical facts the corresponding checks rest on, each checked by the kernel.

signed/bin-packing-volume-bound

TheoremFor all inputsNo axiomsSource

signed/bin-packing-volume-bound :
  (w : ℕ → ℚ) (C g : ℚ) (X : ℕ → ℕ → ℚ) (Kp n : ℕ)
  (hg : 0 < g)
  (hbound : signed/expr-sum-value (fun x₂ => C) Kp + g ≤ signed/expr-sum-value (fun wi => w wi) n)
  (hcols : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), signed/expr-sum-value (fun ck => X ck idx) Kp = 1)
  (hloads : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx Kp), signed/expr-sum-value (fun li => X idx li · w li) n ≤ C)
  → proposition/falsity

+ = signed/add0 = signed/zero1 = signed/one< = signed/less-than= = signed/equivalent: equality of rational values· = signed/multiplyℕ = data/Natℚ = signed/SignedRational≤ = signed/at-most