GrowthInGroups: Characterise 1-approximate subgroups from the no-doub…

…ling classification

LeanCamCombi/GrowthInGroups/ApproximateSubgroup.lean

@@ -5,6 +5,7 @@ import Mathlib.Combinatorics.Additive.RuzsaCovering
 import Mathlib.Combinatorics.Additive.SmallTripling
 import Mathlib.Tactic.Bound
 import LeanCamCombi.Mathlib.Data.Set.Lattice
+import LeanCamCombi.GrowthInGroups.NoDoubling
 
 -- TODO: Unsimp in mathlib
 attribute [-simp] Set.image_subset_iff
@@ -55,6 +56,10 @@ lemma card_pow_le [DecidableEq G] {A : Finset G} (hA : IsApproximateSubgroup K (
       _ ≤ #F ^ (n + 1) * #A := by gcongr; exact mod_cast Finset.card_pow_le
       _ ≤ K ^ (n + 1) * #A := by gcongr
 
+@[to_additive]
+lemma card_mul_self_le [DecidableEq G] {A : Finset G} (hA : IsApproximateSubgroup K (A : Set G)) :
+    #(A * A) ≤ K * #A := by simpa [sq] using hA.card_pow_le (n := 2)
+
 @[to_additive]
 lemma image {F H : Type*} [Group H] [FunLike F G H] [MonoidHomClass F G H] (f : F)
     (hA : IsApproximateSubgroup K A) : IsApproximateSubgroup K (f '' A) where
@@ -151,11 +156,25 @@ lemma pow_inter_pow (hA : IsApproximateSubgroup K A) (hB : IsApproximateSubgroup
 
 end IsApproximateSubgroup
 
-@[to_additive (attr := simp)]
-lemma isApproximateSubgroup_one {S : Type*} [SetLike S G] [SubgroupClass S G] {A : Set G} :
-    IsApproximateSubgroup 1 (A : Set G) ↔ ∃ H : Subgroup G, A = H := by
-  refine ⟨fun hA ↦ ?_, by rintro ⟨H, rfl⟩; exact .subgroup⟩
-  sorry
+open MulAction in
+/-- A finite `1`-approximate subgroup is the same thing as a finite subgroup.
+
+Note that various sources claim this with no proof, some of them without the necessary assumptions
+to make it true (eg Wikipedia before I fixed it). -/
+@[to_additive (attr := simp)
+"A finite `1`-approximate subgroup is the same thing as a finite subgroup.
+
+Note that various sources claim this with no proof, some of them without the necessary assumptions
+to make it true (eg Wikipedia before I fixed it)."]
+lemma isApproximateSubgroup_one {S : Type*} [SetLike S G] [SubgroupClass S G] {A : Set G}
+    (hA : A.Finite) :
+    IsApproximateSubgroup 1 (A : Set G) ↔ ∃ H : Subgroup G, H = A where
+  mp hA' := by
+    classical
+    lift A to Finset G using hA
+    exact ⟨stabilizer G A, by simpa using
+      Finset.smul_stabilizer_of_no_doubling (by simpa using hA'.card_mul_self_le) hA'.one_mem⟩
+  mpr := by rintro ⟨H, rfl⟩; exact .subgroup
 
 open Finset in
 open scoped RightActions in

LeanCamCombi/GrowthInGroups/Lecture1.lean

@@ -69,7 +69,8 @@ open MulAction in
 open scoped RightActions in
 lemma fact_3_10 (hA : #(A * A) ≤ #A) :
     ∃ H : Subgroup G, ∀ a ∈ A, a •> (H : Set G) = A ∧ (H : Set G) <• a = A :=
-  exists_subgroup_of_no_doubling hA
+  ⟨stabilizer G A, fun _a ha ↦
+    ⟨smul_stabilizer_of_no_doubling hA ha, op_smul_stabilizer_of_no_doubling hA ha⟩⟩
 
 open scoped Classical RightActions in
 lemma lemma_3_11 (hA : #(A * A) < (3 / 2 : ℚ) * #A) :

LeanCamCombi/GrowthInGroups/NoDoubling.lean

@@ -17,32 +17,41 @@ open MulOpposite MulAction
 open scoped Pointwise RightActions
 
 namespace Finset
-variable {G : Type*} [Group G] [DecidableEq G] {A : Finset G}
+variable {G : Type*} [Group G] [DecidableEq G] {A : Finset G} {a : G}
 
-/-- A set with no doubling is either empty or the translate of a subgroup. -/
-@[to_additive "A set with no doubling is either empty or the translate of a subgroup."]
-lemma exists_subgroup_of_no_doubling (hA : #(A * A) ≤ #A) :
-    ∃ H : Subgroup G, ∀ a ∈ A, a •> (H : Set G) = A ∧ (H : Set G) <• a = A := by
+@[to_additive]
+private lemma smul_stabilizer_of_no_doubling_aux (hA : #(A * A) ≤ #A) (ha : a ∈ A) :
+    a •> (stabilizer G A : Set G) = A ∧ (stabilizer G A : Set G) <• a = A := by
   have smul_A {a} (ha : a ∈ A) : a •> A = A * A :=
     eq_of_subset_of_card_le (smul_finset_subset_mul ha) (by simpa)
   have op_smul_A {a} (ha : a ∈ A) : A <• a = A * A :=
     eq_of_subset_of_card_le (op_smul_finset_subset_mul ha) (by simpa)
   have smul_A_eq_op_smul_A {a} (ha : a ∈ A) : a •> A = A <• a := by rw [smul_A ha, op_smul_A ha]
-  have smul_A_eq_op_smul_A' {a} (ha : a ∈ A) : a⁻¹ •> A = A <• a⁻¹ := by
-    rw [inv_smul_eq_iff, smul_comm, smul_A_eq_op_smul_A ha, op_inv, inv_smul_smul]
+  have mul_mem_A_comm {x a} (ha : a ∈ A) : x * a ∈ A ↔ a * x ∈ A := by
+    rw [← smul_mem_smul_finset_iff a, smul_A_eq_op_smul_A ha, ← op_smul_eq_mul, smul_comm,
+      smul_mem_smul_finset_iff, smul_eq_mul]
   let H := stabilizer G A
   have inv_smul_A {a} (ha : a ∈ A) : a⁻¹ • (A : Set G) = H := by
     ext x
-    refine ⟨?_, fun hx ↦ ?_⟩
-    · rintro ⟨b, hb, rfl⟩
-      simp [H, mul_smul, inv_smul_eq_iff, smul_A ha, smul_A hb]
+    rw [Set.mem_inv_smul_set_iff, smul_eq_mul]
+    refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
+    · simpa [← smul_A ha, mul_smul] using smul_A hx
     · norm_cast
-      rwa [smul_A_eq_op_smul_A' ha, op_inv, mem_inv_smul_finset_iff, op_smul_eq_mul, ← smul_eq_mul,
-        ← mem_inv_smul_finset_iff, inv_mem hx]
-  refine ⟨H, fun a ha ↦ ⟨?_, ?_⟩⟩
+      rwa [← mul_mem_A_comm ha, ← smul_eq_mul, ← mem_inv_smul_finset_iff, inv_mem hx]
+  refine ⟨?_, ?_⟩
   · rw [← inv_smul_A ha, smul_inv_smul]
   · rw [← inv_smul_A ha, smul_comm]
     norm_cast
     rw [← smul_A_eq_op_smul_A ha, inv_smul_smul]
 
+/-- A non-empty set with no doubling is the left translate of its stabilizer. -/
+@[to_additive "A non-empty set with no doubling is the left-translate of its stabilizer."]
+lemma smul_stabilizer_of_no_doubling (hA : #(A * A) ≤ #A) (ha : a ∈ A) :
+    a •> (stabilizer G A : Set G) = A := (smul_stabilizer_of_no_doubling_aux hA ha).1
+
+/-- A non-empty set with no doubling is the right translate of its stabilizer. -/
+@[to_additive "A non-empty set with no doubling is the right translate of its stabilizer."]
+lemma op_smul_stabilizer_of_no_doubling (hA : #(A * A) ≤ #A) (ha : a ∈ A) :
+    (stabilizer G A : Set G) <• a = A := (smul_stabilizer_of_no_doubling_aux hA ha).2
+
 end Finset