theorem AdditiveCombinatorics.plunnecke_inequality {Z : Type u_1} [DecidableEq Z] [AddCommGroup Z] {A B : Finset Z} (hA : A.Nonempty) {K : ℚ≥0} (hK : ↑(A + B).card ≤ K * ↑A.card) (m n : ℕ) : ↑(m • B - n • B).card ≤ K ^ (m + n) * ↑A.card

Plünnecke–Ruzsa inequality. Let Z be an abelian group and A, B ⊂ Z finite sets with $|A + B| \le K|A|$. Then for any natural numbers m, n, $$|B^{\oplus m} - B^{\oplus n}| \le K^{m+n}\, |A|,$$ where $B^{\oplus k} = k \cdot B$ denotes the k-fold sumset of B with itself.