Sets with very small doubling

For a finset A in a group, its doubling is #(A * A) / #A. This file characterises sets with

• no doubling as the sets which are either empty or translates of a subgroup. For the converse, use the existing facts from the pointwise API: ∅ ^ 2 = ∅ (Finset.empty_pow), (a • H) ^ 2 = a ^ 2 • H ^ 2 = a ^ 2 • H (smul_pow, coe_set_pow).
• doubling strictly less than 3 / 2 as the sets that are contained in a coset of a subgroup of size strictly less than 3 / 2 * #A.
• doubling strictly less than φ as the set A such that A * A⁻¹ is covered by at most some constant (depending only on the doubling) number of cosets of a finite subgroup of G.

TODO

• Do we need versions stated using the doubling constant (Finset.mulConst)?
• Add characterisation of sets with doubling ≤ 2 - ε. See https://terrytao.wordpress.com/2011/03/12/hamidounes-freiman-kneser-theorem-for-nonabelian-groups.

References

• An elementary non-commutative Freiman theorem, Terence Tao
• Introduction to approximate groups, Matthew Tointon

Doubling exactly 1

theorem Finset.smul_stabilizer_of_no_doubling {G : Type u_1} [Group G] [DecidableEq G] {A : Finset G} {a : G} (hA : (A * A).card ≤ A.card) (ha : a ∈ A) : a • ↑(MulAction.stabilizer G A) = ↑A

A non-empty set with no doubling is the left translate of its stabilizer.

theorem Finset.vadd_stabilizer_of_no_doubling {G : Type u_1} [AddGroup G] [DecidableEq G] {A : Finset G} {a : G} (hA : (A + A).card ≤ A.card) (ha : a ∈ A) : a +ᵥ ↑(AddAction.stabilizer G A) = ↑A

A non-empty set with no doubling is the left-translate of its stabilizer.

theorem Finset.op_smul_stabilizer_of_no_doubling {G : Type u_1} [Group G] [DecidableEq G] {A : Finset G} {a : G} (hA : (A * A).card ≤ A.card) (ha : a ∈ A) : MulOpposite.op a • ↑(MulAction.stabilizer G A) = ↑A

A non-empty set with no doubling is the right translate of its stabilizer.

theorem Finset.op_vadd_stabilizer_of_no_doubling {G : Type u_1} [AddGroup G] [DecidableEq G] {A : Finset G} {a : G} (hA : (A + A).card ≤ A.card) (ha : a ∈ A) : AddOpposite.op a +ᵥ ↑(AddAction.stabilizer G A) = ↑A

A non-empty set with no doubling is the right translate of its stabilizer.

Doubling strictly less than 3 / 2

theorem Finset.mul_inv_eq_inv_mul_of_doubling_lt_two {G : Type u_1} [Group G] [DecidableEq G] {A : Finset G} (h : (A * A).card < 2 * A.card) : A * A⁻¹ = A⁻¹ * A

If A has doubling strictly less than 2, then A * A⁻¹ = A⁻¹ * A.

def Finset.invMulSubgroup {G : Type u_1} [Group G] [DecidableEq G] (A : Finset G) (h : ↑(A * A).card < 3 / 2 * ↑A.card) : Subgroup G

If A has doubling strictly less than 3 / 2, then A⁻¹ * A is a subgroup.

Note that this is sharp: A = {0, 1} in ℤ has doubling 3 / 2 and A⁻¹ * A isn't a subgroup.

Equations

• A.invMulSubgroup h = { carrier := ↑A⁻¹ * ↑A, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

theorem Finset.invMulSubgroup_eq_inv_mul {G : Type u_1} [Group G] [DecidableEq G] (A : Finset G) (h : ↑(A * A).card < 3 / 2 * ↑A.card) : ↑(A.invMulSubgroup h) = ↑A⁻¹ * ↑A

theorem Finset.invMulSubgroup_eq_mul_inv {G : Type u_1} [Group G] [DecidableEq G] (A : Finset G) (h : ↑(A * A).card < 3 / 2 * ↑A.card) : ↑(A.invMulSubgroup h) = ↑A * ↑A⁻¹

instance Finset.instFintypeSubtypeMemSubgroupInvMulSubgroup {G : Type u_1} [Group G] [DecidableEq G] (A : Finset G) (h : ↑(A * A).card < 3 / 2 * ↑A.card) : Fintype ↥(A.invMulSubgroup h)

Equations

• A.instFintypeSubtypeMemSubgroupInvMulSubgroup h = ⋯.mpr inferInstance

theorem Finset.smul_inv_mul_opSMul_eq_mul_of_doubling_lt_three_halves {G : Type u_1} [Group G] [DecidableEq G] {A : Finset G} {a : G} (h : ↑(A * A).card < 3 / 2 * ↑A.card) (ha : a ∈ A) : a • MulOpposite.op a • (A⁻¹ * A) = A * A

theorem Finset.card_inv_mul_of_doubling_lt_three_halves {G : Type u_1} [Group G] [DecidableEq G] {A : Finset G} (h : ↑(A * A).card < 3 / 2 * ↑A.card) : (A⁻¹ * A).card = (A * A).card

theorem Finset.smul_inv_mul_eq_inv_mul_opSMul {G : Type u_1} [Group G] [DecidableEq G] {A : Finset G} {a : G} (h : ↑(A * A).card < 3 / 2 * ↑A.card) (ha : a ∈ A) : a • (A⁻¹ * A) = MulOpposite.op a • (A⁻¹ * A)

theorem Finset.doubling_lt_three_halves {G : Type u_1} [Group G] [DecidableEq G] {A : Finset G} (h : ↑(A * A).card < 3 / 2 * ↑A.card) : ∃ (H : Subgroup G) (x : Fintype ↥H), ↑(Fintype.card ↥H) < 3 / 2 * ↑A.card ∧ ∀ a ∈ A, ↑A ⊆ a • ↑H ∧ a • ↑H = MulOpposite.op a • ↑H

If A has doubling strictly less than 3 / 2, then there exists a subgroup H of the normaliser of A of size strictly less than 3 / 2 * #A such that A is a subset of a coset of H (in fact a subset of a • H for every a ∈ A).

Note that this is sharp: A = {0, 1} in ℤ has doubling 3 / 2 and can't be covered by a subgroup of size at most 2.

This is Theorem 2.2.1 in [Toi20].

Doubling strictly less than φ

theorem Finset.doubling_lt_golden_ratio {G : Type u_1} [Group G] [DecidableEq G] {K : ℝ} {A : Finset G} (hK₁ : 1 < K) (hKφ : K < Real.goldenRatio) (hA₁ : ↑(A⁻¹ * A).card ≤ K * ↑A.card) (hA₂ : ↑(A * A⁻¹).card ≤ K * ↑A.card) : ∃ (H : Subgroup G) (x : Fintype ↥H) (Z : Finset G), ↑Z.card ≤ (2 - K) * K / ((Real.goldenRatio - K) * (K - Real.goldenConj)) ∧ ↑H * ↑Z = ↑A * ↑A⁻¹

If A has doubling K strictly less than φ, then A * A⁻¹ is covered by at most a constant number of cosets of a finite subgroup of G.

Doubling less than 2-ε

theorem Finset.card_mul_finset_lt_two {G : Type u_1} [Group G] [DecidableEq G] {S : Finset G} {ε : ℝ} (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (hS : S.Nonempty) (hA : ∃ (A : Finset G), S.card ≤ A.card ∧ ↑(A * S).card ≤ (2 - ε) * ↑S.card) : ∃ (H : Subgroup G) (x : Fintype ↥H) (Z : Finset G), ↑(Fintype.card ↥H) ≤ (2 / ε - 1) * ↑S.card ∧ ↑Z.card ≤ 2 / ε - 1 ∧ ↑S ⊆ ↑H * ↑Z

If S is nonempty such that there is A with |S| ≤ |A| such that |A * S| ≤ (2 - ε) * |S| for some 0 < ε ≤ 1, then there is a finite subgroup H of G of size |H| ≤ (2 / ε - 1) * |S| such that S is covered by at most 2 / ε - 1 right cosets of H.

theorem Finset.doubling_lt_two {G : Type u_1} [Group G] [DecidableEq G] {A : Finset G} {ε : ℝ} (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (hA₀ : A.Nonempty) (hA₁ : ↑(A * A).card ≤ (2 - ε) * ↑A.card) : ∃ (H : Subgroup G) (x : Fintype ↥H) (Z : Finset G), ↑(Fintype.card ↥H) ≤ (2 / ε - 1) * ↑A.card ∧ ↑Z.card ≤ 2 / ε - 1 ∧ ↑A ⊆ ↑H * ↑Z

Corollary of card_mul_finset_lt_two in the case A = S, giving characterisation of sets of doubling less than 2 - ε.