Splitting a finite sum of bounded natural weights

If each item has weight at most M and the total is at least 2 * k + M, a subset and its complement both have weight at least k. A first subset reaching k overshoots by at most M - 1, leaving enough weight in its complement.

Main results

• Finset.exists_subset_sum_ge: a balanced split of bounded natural-number weights.

References

• S. Schlesinger, Algebraic circuit formalizations in Complexitylib, Threshold/Internal/Excess

theorem Finset.exists_subset_sum_ge {ι : Type u_1} [DecidableEq ι] (𝓑 : Finset ι) (φ : ι → ℕ) (M k : ℕ) (hφ : ∀ b ∈ 𝓑, φ b ≤ M) (htot : 2 * k + M ≤ ∑ b ∈ 𝓑, φ b) : ∃ 𝒢 ⊆ 𝓑, k ≤ ∑ b ∈ 𝒢, φ b ∧ k ≤ ∑ b ∈ 𝓑 \ 𝒢, φ b

Subset sum. Items of weight at most M with total weight at least 2 * k + M can be partitioned into 𝒢 ⊆ 𝓑 and 𝓑 \ 𝒢 each of weight at least k.