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.

TODO

• Do we need versions stated using the doubling constant (Finset.mulConst)?
• Add characterisation of sets with doubling < φ. See https://terrytao.wordpress.com/2009/11/10/an-elementary-non-commutative-freiman-theorem.
• 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][tointon2020]

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 [tointon2020].