Duality between packings and rows: the finite core

• sum_mul_sum_mem — double counting ∑_S κ_S a(S) = ∑_i a_i ∑_{S ∋ i} κ_S;
• no_separator — if every fractional packing has value at most K, then no κ ≥ 0 has ∑_S κ_S (a(S) - t_S) < 0 for all a ≥ 0 of mass at most K.

In no_separator, write c = ∑_S κ_S t_S and M_i = ∑_{S ∋ i} κ_S. The hypothesis reads ∑_i a_i M_i < c for all admissible a; a = 0 gives c > 0. Case A (no M_i is positive): ((K+1)/c) κ is a packing of value K + 1 > K. Case B (M_j = max_i M_i > 0): κ / M_j is a packing, so c ≤ K M_j, while a = K e_j gives K M_j < c.

This is the part of the proof of Proposition 6.7 (Duality) of the paper which follows the separation step; there c and M_i are written ϑ and σ_i.

theorem AaronsonAmbainis.Dual.sum_mul_sum_mem {ι : Type u_1} [Fintype ι] [DecidableEq ι] (κ : Finset ι → ℝ) (a : ι → ℝ) : ∑ S : Finset ι, κ S * ∑ i ∈ S, a i = ∑ i : ι, a i * ∑ S : Finset ι with i ∈ S, κ S

theorem AaronsonAmbainis.Dual.no_separator {ι : Type u_1} [Fintype ι] [DecidableEq ι] (t : Finset ι → ℝ) (K : ℝ) (hK : 0 ≤ K) (hpack : ∀ (κ : Finset ι → ℝ), (∀ (S : Finset ι), 0 ≤ κ S) → (∀ (i : ι), ∑ S : Finset ι with i ∈ S, κ S ≤ 1) → ∑ S : Finset ι, κ S * t S ≤ K) (κ : Finset ι → ℝ) (hκ : ∀ (S : Finset ι), 0 ≤ κ S) (hsep : ∀ (a : ι → ℝ), (∀ (i : ι), 0 ≤ a i) → ∑ i : ι, a i ≤ K → ∑ S : Finset ι, κ S * (∑ i ∈ S, a i - t S) < 0) : False