Theorems · Theorem · combinatorics

Finset.small_nsmul_of_small_tripling

∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddGroup G] {A : Finset G} {K : ℝ} {m : ℕ},
  3 ≤ m → ↑(3 • A).card ≤ K * ↑A.card → -A = A → ↑(m • A).card ≤ K ^ (m - 2) * ↑A.card

If A is symmetric (-A = A) and has small tripling, then A has small powers, in the sense that |m • A| is at most |A| times a constant exponential in m. See also Finset.small_alternating_nsmul_of_small_tripling for a version with a weaker constant but which encompasses non-symmetric sets.

Defined in

Mathlib.Combinatorics.Additive.SmallTripling

Cited by

1 results in Mathlib

Foundations

Depth 107 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqAddGroup