Small tripling implies small powers

This file shows that a set with small tripling has small powers, even in non-abelian groups.

See also

In abelian groups, the Plünnecke-Ruzsa inequality is the stronger statement that small doubling implies small powers. See Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean.

theorem Finset.small_alternating_pow_of_small_tripling {G : Type u_1} [DecidableEq G] [Group G] {A : Finset G} {K : ℝ} {m : ℕ} (hm : 3 ≤ m) (hA : ↑(A ^ 3).card ≤ K * ↑A.card) (ε : Fin m → ℤ) (hε : ∀ (i : Fin m), |ε i| = 1) : ↑(List.map (fun (i : Fin m) => A ^ ε i) (List.finRange m)).prod.card ≤ K ^ (3 * (m - 2)) * ↑A.card

If A has small tripling, say with constant K, then A has small alternating powers, in the sense that |A^±1 * ... * A^±1| is at most |A| times a constant exponential in the number of terms in the product.

When A is symmetric (A⁻¹ = A), the base of the exponential can be lowered from K ^ 3 to K, where K is the tripling constant. See Finset.small_pow_of_small_tripling.

theorem Finset.small_alternating_nsmul_of_small_tripling {G : Type u_1} [DecidableEq G] [AddGroup G] {A : Finset G} {K : ℝ} {m : ℕ} (hm : 3 ≤ m) (hA : ↑(3 • A).card ≤ K * ↑A.card) (ε : Fin m → ℤ) (hε : ∀ (i : Fin m), |ε i| = 1) : ↑(List.map (fun (i : Fin m) => ε i • A) (List.finRange m)).sum.card ≤ K ^ (3 * (m - 2)) * ↑A.card

If A has small tripling, say with constant K, then A has small alternating powers, in the sense that |±A ± ... ± A| is at most |A| times a constant exponential in the number of terms in the product.

When A is symmetric (-A = A), the base of the exponential can be lowered from K ^ 3 to K, where K is the tripling constant. See Finset.small_nsmul_of_small_tripling.

theorem Finset.small_pow_of_small_tripling {G : Type u_1} [DecidableEq G] [Group G] {A : Finset G} {K : ℝ} {m : ℕ} (hm : 3 ≤ m) (hA : ↑(A ^ 3).card ≤ K * ↑A.card) (hAsymm : A⁻¹ = A) : ↑(A ^ m).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 |A ^ m| is at most |A| times a constant exponential in m.

See also Finset.small_alternating_pow_of_small_tripling for a version with a weaker constant but which encompasses non-symmetric sets.

theorem Finset.small_nsmul_of_small_tripling {G : Type u_1} [DecidableEq G] [AddGroup G] {A : Finset G} {K : ℝ} {m : ℕ} (hm : 3 ≤ m) (hA : ↑(3 • A).card ≤ K * ↑A.card) (hAsymm : -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.