Duality between packings and rows

Dual.exists_cover is Proposition 6.7 (Duality) of the paper. coverDuality : CoverDuality follows from it: CoverDuality is the same statement with the two side hypotheses 0 ≤ K and t ∅ ≤ 0 (neither is needed: the zero packing gives 0 ≤ K, and t ∅ ≤ 0 is the conclusion at S = ∅).

Proof of Dual.exists_cover. Let P = Dual.massSet ι K = {a ≥ 0, ∑ a ≤ K} and Q = Dual.slack t '' P, the set of all slack vectors S ↦ a(S) - t S; the claim is that Q meets the nonnegative orthant of Finset ι → ℝ. If not, the geometric Hahn–Banach theorem (geometric_hahn_banach_compact_closed: Q is compact and convex, the orthant is closed and convex) gives a continuous linear functional φ and reals u < r with φ < u on Q and r < φ on the orthant. Then r < 0, the coefficients κ_S = φ (e_S) are nonnegative (Dual.coeff_nonneg), φ v = ∑_S κ_S v_S (Dual.functional_eq_sum), and ∑_S κ_S (a(S) - t_S) < u < 0 for all a ∈ P, which Dual.no_separator excludes.

In the paper the set Q is called C, and the vector κ is obtained from Lemma 6.6 (Separation from the orthant), for which the paper gives a short direct proof; here Mathlib's geometric Hahn–Banach theorem takes the place of that lemma.

theorem AaronsonAmbainis.Dual.exists_cover {ι : Type u_1} [Fintype ι] [DecidableEq ι] (t : Finset ι → ℝ) (K : ℝ) (hpack : ∀ (κ : Finset ι → ℝ), (∀ (S : Finset ι), 0 ≤ κ S) → (∀ (i : ι), ∑ S : Finset ι with i ∈ S, κ S ≤ 1) → ∑ S : Finset ι, κ S * t S ≤ K) : ∃ (a : ι → ℝ), (∀ (i : ι), 0 ≤ a i) ∧ ∑ i : ι, a i ≤ K ∧ ∀ (S : Finset ι), t S ≤ ∑ i ∈ S, a i

Linear-programming duality between fractional packings and rows: if every fractional packing κ has ∑_S κ_S t_S ≤ K, then some a ≥ 0 of total mass at most K has t_S ≤ a(S) for every S.

theorem AaronsonAmbainis.coverDuality : CoverDuality