Approximate subgroups

This file defines approximate subgroups of a group, namely symmetric sets A such that A * A can be covered by a small number of translates of A.

Main results

Approximate subgroups are a central concept in additive combinatorics, as a natural weakening and flexible substitute of genuine subgroups. As such, they share numerous properties with subgroups:

• IsApproximateSubgroup.image: Group homomorphisms send approximate subgroups to approximate subgroups
• IsApproximateSubgroup.pow_inter_pow: The intersection of (non-trivial powers of) two approximate subgroups is an approximate subgroup. Warning: The intersection of two approximate subgroups isn't an approximate subgroup in general.

Approximate subgroups are close qualitatively and quantitatively to other concepts in additive combinatorics:

• IsApproximateSubgroup.card_pow_le: An approximate subgroup has small powers.
• IsApproximateSubgroup.of_small_tripling: A set of small tripling can be made an approximate subgroup by squaring.

It can be readily confirmed that approximate subgroups are a weakening of subgroups:

• isApproximateSubgroup_one: A 1-approximate subgroup is the same thing as a subgroup.

structure IsApproximateAddSubgroup {G : Type u_2} [AddGroup G] (K : ℝ) (A : Set G) : Prop

An approximate subgroup in a group is a symmetric set A containing the identity and such that A + A can be covered by a small number of translates of A.

In practice, we will take K fixed and A large but finite.

• zero_mem : 0 ∈ A
• neg_eq_self : -A = A
• two_nsmul_covByVAdd : CovByVAdd G K (2 • A) A

structure IsApproximateSubgroup {G : Type u_1} [Group G] (K : ℝ) (A : Set G) : Prop

An approximate subgroup in a group is a symmetric set A containing the identity and such that A * A can be covered by a small number of translates of A.

In practice, we will take K fixed and A large but finite.

• one_mem : 1 ∈ A
• inv_eq_self : A⁻¹ = A
• sq_covBySMul : CovBySMul G K (A ^ 2) A

theorem IsApproximateSubgroup.nonempty {G : Type u_1} [Group G] {A : Set G} {K : ℝ} (hA : IsApproximateSubgroup K A) : A.Nonempty

theorem IsApproximateAddSubgroup.nonempty {G : Type u_1} [AddGroup G] {A : Set G} {K : ℝ} (hA : IsApproximateAddSubgroup K A) : A.Nonempty

theorem IsApproximateSubgroup.one_le {G : Type u_1} [Group G] {A : Set G} {K : ℝ} (hA : IsApproximateSubgroup K A) : 1 ≤ K

theorem IsApproximateAddSubgroup.one_le {G : Type u_1} [AddGroup G] {A : Set G} {K : ℝ} (hA : IsApproximateAddSubgroup K A) : 1 ≤ K

theorem IsApproximateSubgroup.mono {G : Type u_1} [Group G] {A : Set G} {K L : ℝ} (hKL : K ≤ L) (hA : IsApproximateSubgroup K A) : IsApproximateSubgroup L A

theorem IsApproximateAddSubgroup.mono {G : Type u_1} [AddGroup G] {A : Set G} {K L : ℝ} (hKL : K ≤ L) (hA : IsApproximateAddSubgroup K A) : IsApproximateAddSubgroup L A

theorem IsApproximateSubgroup.card_pow_le {G : Type u_1} [Group G] {K : ℝ} [DecidableEq G] {A : Finset G} (hA : IsApproximateSubgroup K ↑A) {n : ℕ} : ↑(A ^ n).card ≤ K ^ (n - 1) * ↑A.card

theorem IsApproximateAddSubgroup.card_nsmul_le {G : Type u_1} [AddGroup G] {K : ℝ} [DecidableEq G] {A : Finset G} (hA : IsApproximateAddSubgroup K ↑A) {n : ℕ} : ↑(n • A).card ≤ K ^ (n - 1) * ↑A.card

theorem IsApproximateSubgroup.card_mul_self_le {G : Type u_1} [Group G] {K : ℝ} [DecidableEq G] {A : Finset G} (hA : IsApproximateSubgroup K ↑A) : ↑(A * A).card ≤ K * ↑A.card

theorem IsApproximateAddSubgroup.card_add_self_le {G : Type u_1} [AddGroup G] {K : ℝ} [DecidableEq G] {A : Finset G} (hA : IsApproximateAddSubgroup K ↑A) : ↑(A + A).card ≤ K * ↑A.card

theorem IsApproximateSubgroup.image {G : Type u_1} [Group G] {A : Set G} {K : ℝ} {F : Type u_2} {H : Type u_3} [Group H] [FunLike F G H] [MonoidHomClass F G H] (f : F) (hA : IsApproximateSubgroup K A) : IsApproximateSubgroup K (⇑f '' A)

theorem IsApproximateAddSubgroup.image {G : Type u_1} [AddGroup G] {A : Set G} {K : ℝ} {F : Type u_2} {H : Type u_3} [AddGroup H] [FunLike F G H] [AddMonoidHomClass F G H] (f : F) (hA : IsApproximateAddSubgroup K A) : IsApproximateAddSubgroup K (⇑f '' A)

theorem IsApproximateSubgroup.subgroup {G : Type u_1} [Group G] {S : Type u_2} [SetLike S G] [SubgroupClass S G] {H : S} : IsApproximateSubgroup 1 ↑H

theorem IsApproximateAddSubgroup.addSubgroup {G : Type u_1} [AddGroup G] {S : Type u_2} [SetLike S G] [AddSubgroupClass S G] {H : S} : IsApproximateAddSubgroup 1 ↑H

theorem IsApproximateSubgroup.of_small_tripling {G : Type u_1} [Group G] {K : ℝ} [DecidableEq G] {A : Finset G} (hA₁ : 1 ∈ A) (hAsymm : A⁻¹ = A) (hA : ↑(A ^ 3).card ≤ K * ↑A.card) : IsApproximateSubgroup (K ^ 3) (↑A ^ 2)

theorem IsApproximateAddSubgroup.of_small_tripling {G : Type u_1} [AddGroup G] {K : ℝ} [DecidableEq G] {A : Finset G} (hA₁ : 0 ∈ A) (hAsymm : -A = A) (hA : ↑(3 • A).card ≤ K * ↑A.card) : IsApproximateAddSubgroup (K ^ 3) (2 • ↑A)

theorem IsApproximateSubgroup.pow_inter_pow_covBySMul_sq_inter_sq {G : Type u_1} [Group G] {A B : Set G} {K L : ℝ} {m n : ℕ} (hA : IsApproximateSubgroup K A) (hB : IsApproximateSubgroup L B) (hm : 2 ≤ m) (hn : 2 ≤ n) : CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (A ^ 2 ∩ B ^ 2)

theorem IsApproximateAddSubgroup.nsmul_inter_nsmul_covByVAdd_sq_inter_sq {G : Type u_1} [AddGroup G] {A B : Set G} {K L : ℝ} {m n : ℕ} (hA : IsApproximateAddSubgroup K A) (hB : IsApproximateAddSubgroup L B) (hm : 2 ≤ m) (hn : 2 ≤ n) : CovByVAdd G (K ^ (m - 1) * L ^ (n - 1)) (m • A ∩ n • B) (2 • A ∩ 2 • B)

theorem IsApproximateSubgroup.pow_inter_pow {G : Type u_1} [Group G] {A B : Set G} {K L : ℝ} {m n : ℕ} (hA : IsApproximateSubgroup K A) (hB : IsApproximateSubgroup L B) (hm : 2 ≤ m) (hn : 2 ≤ n) : IsApproximateSubgroup (K ^ (2 * m - 1) * L ^ (2 * n - 1)) (A ^ m ∩ B ^ n)

theorem IsApproximateAddSubgroup.nsmul_inter_nsmul {G : Type u_1} [AddGroup G] {A B : Set G} {K L : ℝ} {m n : ℕ} (hA : IsApproximateAddSubgroup K A) (hB : IsApproximateAddSubgroup L B) (hm : 2 ≤ m) (hn : 2 ≤ n) : IsApproximateAddSubgroup (K ^ (2 * m - 1) * L ^ (2 * n - 1)) (m • A ∩ n • B)

@[simp]

theorem isApproximateSubgroup_one {G : Type u_1} [Group G] {A : Set G} : IsApproximateSubgroup 1 A ↔ ∃ (H : Subgroup G), ↑H = A

A 1-approximate subgroup is the same thing as a subgroup.

@[simp]

theorem isApproximateAddSubgroup_zero {G : Type u_1} [AddGroup G] {A : Set G} : IsApproximateAddSubgroup 1 A ↔ ∃ (H : AddSubgroup G), ↑H = A

A 1-approximate subgroup is the same thing as a subgroup.