The row bound from the packing bound and duality

Dual.rowBoundPM_of_packing_of_cover : PackingBound → CoverDuality → RowBoundPM (Theorem 6.8 of the paper from Lemma 6.5 and linear-programming duality, Proposition 6.7). As in the paper, at each point x duality is applied to the demands t S = |f x - f (x^S)| with K = π² d²; then S = Δ(x,y).

theorem AaronsonAmbainis.Dual.rowBoundPM_of_packing_of_cover : PackingBound → CoverDuality → RowBoundPM