theorem PlunneckeInequality.poly_k_growth (s t : ℝ) (hs : 0 < s) (hst : s < t) (ht : t < 1) : ∃ (K : ℕ), ∀ (p : ℕ) [Fact (Nat.Prime p)] (A : Finset (ZMod p)), ↑A.card = ↑p ^ s → ↑(poly_k K A).card ≥ ↑p ^ t

Polynomial growth corollary. If 0 < s < t < 1, then there exists K = K(s,t) such that for every prime p and every A ⊆ 𝔽_p with |A| = p^s we have |poly_K(A)| ≥ p^t.