def PlunneckeInequality.poly_k {G : Type u_1} [CommRing G] [DecidableEq G] (K : ℕ) (A : Finset G) : Finset G

The set poly_K(A) = (A^K)^{⊕K} - (A^K)^{⊕K}, i.e. the difference of the K-fold iterated sumset of the K-fold product set A^K. This is the auxiliary polynomial-growth set used in the Plünnecke / Bourgain–Katz–Tao expansion arguments.