GrowthInGroups: Half of lecture 3

Author: YaelDillies

LeanCamCombi/GrowthInGroups/ApproximateSubgroup.lean

@@ -1,73 +1,102 @@
-import Mathlib.Algebra.Group.Subgroup.Defs
 import Mathlib.Algebra.Order.BigOperators.Ring.Finset
 import Mathlib.Combinatorics.Additive.SmallTripling
+import Mathlib.Tactic.Bound
 import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
 import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.Basic
+import LeanCamCombi.Mathlib.Algebra.Group.Subgroup.Pointwise
 import LeanCamCombi.Mathlib.Combinatorics.Additive.RuzsaCovering
 import LeanCamCombi.Mathlib.Data.Finset.Basic
+import LeanCamCombi.Mathlib.Data.Set.Basic
+import LeanCamCombi.Mathlib.Data.Set.Lattice
+import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
+
+-- TODO: Unsimp in mathlib
+attribute [-simp] Set.image_subset_iff
 
 open scoped Finset Pointwise
 
-variable {G : Type*} [Group G] {S : Set G} {K L : ℝ} {n : ℕ}
+variable {G : Type*} [Group G] {A B : Set G} {K L : ℝ} {m n : ℕ}
 
-structure IsApproximateAddSubgroup {G : Type*} [AddGroup G] (S : Set G) (K : ℝ) : Prop where
-  nonempty : S.Nonempty
-  neg_eq_self : -S = S
-  exists_two_nsmul_subset_add : ∃ F : Finset G, #F ≤ K ∧ 2 • S ⊆ F + S
+structure IsApproximateAddSubgroup {G : Type*} [AddGroup G] (K : ℝ) (A : Set G) : Prop where
+  nonempty : A.Nonempty
+  neg_eq_self : -A = A
+  exists_two_nsmul_subset_add : ∃ F : Finset G, #F ≤ K ∧ 2 • A ⊆ F + A
 
 @[to_additive]
-structure IsApproximateSubgroup (S : Set G) (K : ℝ) : Prop where
-  nonempty : S.Nonempty
-  inv_eq_self : S⁻¹ = S
-  exists_sq_subset_mul : ∃ F : Finset G, #F ≤ K ∧ S ^ 2 ⊆ F * S
+structure IsApproximateSubgroup (K : ℝ) (A : Set G) : Prop where
+  nonempty : A.Nonempty
+  inv_eq_self : A⁻¹ = A
+  exists_sq_subset_mul : ∃ F : Finset G, #F ≤ K ∧ A ^ 2 ⊆ F * A
 
 namespace IsApproximateSubgroup
 
 @[to_additive one_le]
-lemma one_le (hS : IsApproximateSubgroup S K) : 1 ≤ K := by
-  obtain ⟨F, hF, hSF⟩ := hS.exists_sq_subset_mul
-  have hF₀ : F ≠ ∅ := by rintro rfl; simp [hS.nonempty.pow.ne_empty] at hSF
+lemma one_le (hA : IsApproximateSubgroup K A) : 1 ≤ K := by
+  obtain ⟨F, hF, hSF⟩ := hA.exists_sq_subset_mul
+  have hF₀ : F ≠ ∅ := by rintro rfl; simp [hA.nonempty.pow.ne_empty] at hSF
   exact hF.trans' <| by simpa [Finset.nonempty_iff_ne_empty]
 
 @[to_additive]
-lemma mono (hKL : K ≤ L) (hS : IsApproximateSubgroup S K) : IsApproximateSubgroup S L where
-  nonempty := hS.nonempty
-  inv_eq_self := hS.inv_eq_self
-  exists_sq_subset_mul := let ⟨F, hF, hSF⟩ := hS.exists_sq_subset_mul; ⟨F, hF.trans hKL, hSF⟩
+lemma mono (hKL : K ≤ L) (hA : IsApproximateSubgroup K A) : IsApproximateSubgroup L A where
+  nonempty := hA.nonempty
+  inv_eq_self := hA.inv_eq_self
+  exists_sq_subset_mul := let ⟨F, hF, hSF⟩ := hA.exists_sq_subset_mul; ⟨F, hF.trans hKL, hSF⟩
 
 @[to_additive]
-lemma card_pow_le [DecidableEq G] {S : Finset G} (hS : IsApproximateSubgroup (S : Set G) K) :
-    ∀ {n}, #(S ^ n) ≤ K ^ (n - 1) * #S
-  | 0 => by simpa using hS.nonempty
+lemma card_pow_le [DecidableEq G] {A : Finset G} (hA : IsApproximateSubgroup K (A : Set G)) :
+    ∀ {n}, #(A ^ n) ≤ K ^ (n - 1) * #A
+  | 0 => by simpa using hA.nonempty
   | 1 => by simp
   | n + 2 => by
-    obtain ⟨F, hF, hSF⟩ := hS.exists_sq_subset_mul
+    obtain ⟨F, hF, hSF⟩ := hA.exists_sq_subset_mul
     calc
-      (#(S ^ (n + 2)) : ℝ) ≤ #(F ^ (n + 1) * S) := by
+      (#(A ^ (n + 2)) : ℝ) ≤ #(F ^ (n + 1) * A) := by
         gcongr; exact mod_cast Set.pow_subset_pow_mul_of_sq_subset_mul hSF (by omega)
-      _ ≤ #(F ^ (n + 1)) * #S := mod_cast Finset.card_mul_le
-      _ ≤ #F ^ (n + 1) * #S := by gcongr; exact mod_cast Finset.card_pow_le
-      _ ≤ K ^ (n + 1) * #S := by gcongr
+      _ ≤ #(F ^ (n + 1)) * #A := mod_cast Finset.card_mul_le
+      _ ≤ #F ^ (n + 1) * #A := by gcongr; exact mod_cast Finset.card_pow_le
+      _ ≤ K ^ (n + 1) * #A := by gcongr
 
 @[to_additive]
-lemma pi {ι : Type*} {G : ι → Type*} [Fintype ι] [∀ i, Group (G i)] {S : ∀ i, Set (G i)} {K : ι → ℝ}
-    (hS : ∀ i, IsApproximateSubgroup (S i) (K i)) :
-    IsApproximateSubgroup (Set.univ.pi S) (∏ i, K i) where
-  nonempty := Set.univ_pi_nonempty_iff.2 fun i ↦ (hS i).nonempty
-  inv_eq_self := by simp [(hS _).inv_eq_self]
+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
+  nonempty := hA.nonempty.image _
+  inv_eq_self := by simp [← Set.image_inv', hA.inv_eq_self]
   exists_sq_subset_mul := by
-    choose F hF hFS using fun i ↦ (hS i).exists_sq_subset_mul
+    classical
+    obtain ⟨F, hF, hAF⟩ := hA.exists_sq_subset_mul
+    refine ⟨F.image f, ?_, ?_⟩
+    · calc
+        (#(F.image f) : ℝ) ≤ #F := mod_cast F.card_image_le
+        _ ≤ K := hF
+    · simp only [← Set.image_pow, Finset.coe_image, ← Set.image_mul]
+      gcongr
+
+@[to_additive]
+lemma pi {ι : Type*} {G : ι → Type*} [Fintype ι] [∀ i, Group (G i)] {A : ∀ i, Set (G i)} {K : ι → ℝ}
+    (hA : ∀ i, IsApproximateSubgroup (K i) (A i)) :
+    IsApproximateSubgroup (∏ i, K i) (Set.univ.pi A) where
+  nonempty := Set.univ_pi_nonempty_iff.2 fun i ↦ (hA i).nonempty
+  inv_eq_self := by simp [(hA _).inv_eq_self]
+  exists_sq_subset_mul := by
+    choose F hF hFS using fun i ↦ (hA i).exists_sq_subset_mul
     classical
     refine ⟨Fintype.piFinset F, ?_, ?_⟩
     · calc
         #(Fintype.piFinset F) = ∏ i, (#(F i) : ℝ) := by simp
         _ ≤ ∏ i, K i := by gcongr; exact hF _
     · sorry
 
+@[to_additive]
+lemma subgroup {S : Type*} [SetLike S G] [SubgroupClass S G] {H : S} :
+    IsApproximateSubgroup 1 (H : Set G) where
+  nonempty := .of_subtype
+  inv_eq_self := inv_coe_set
+  exists_sq_subset_mul := ⟨{1}, by simp⟩
+
 open Finset in
 @[to_additive]
 lemma of_small_tripling [DecidableEq G] {A : Finset G} (hA₀ : A.Nonempty) (hAsymm : A⁻¹ = A)
-    (hA : #(A ^ 3) ≤ K * #A) : IsApproximateSubgroup (A ^ 2 : Set G) (K ^ 3) where
+    (hA : #(A ^ 3) ≤ K * #A) : IsApproximateSubgroup (K ^ 3) (A ^ 2 : Set G) where
   nonempty := hA₀.to_set.pow
   inv_eq_self := by simp [← inv_pow, hAsymm, ← coe_inv]
   exists_sq_subset_mul := by
@@ -78,4 +107,67 @@ lemma of_small_tripling [DecidableEq G] {A : Finset G} (hA₀ : A.Nonempty) (hAs
     have hF₀ : F.Nonempty := nonempty_iff_ne_empty.2 <| by rintro rfl; simp [hA₀.ne_empty] at hAF
     exact ⟨F, hF, by norm_cast; simpa [div_eq_mul_inv, pow_succ, mul_assoc, hAsymm] using hAF⟩
 
+open Set in
+@[to_additive]
+lemma exists_pow_inter_pow_subset (hA : IsApproximateSubgroup K A) (hB : IsApproximateSubgroup L B)
+    (hm : 2 ≤ m) (hn : 2 ≤ n) :
+    ∃ F : Finset G, #F ≤ K ^ (m - 1) * L ^ (n - 1) ∧ A ^ m ∩ B ^ n ⊆ F * (A ^ 2 ∩ B ^ 2) := by
+  classical
+  obtain ⟨F₁, hF₁, hAF₁⟩ := hA.exists_sq_subset_mul
+  obtain ⟨F₂, hF₂, hBF₂⟩ := hB.exists_sq_subset_mul
+  have := hA.one_le
+  choose f hf using exists_smul_inter_smul_subset_smul_sq_inter_sq hA.inv_eq_self hB.inv_eq_self
+  refine ⟨.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1)), ?_, ?_⟩
+  · calc
+      (#(.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) : ℝ)
+      _ ≤ #(F₁ ^ (m - 1)) * #(F₂ ^ (n - 1)) := mod_cast Finset.card_image₂_le ..
+      _ ≤ #F₁ ^ (m - 1) * #F₂ ^ (n - 1) := by gcongr <;> exact mod_cast Finset.card_pow_le
+      _ ≤ K ^ (m - 1) * L ^ (n - 1) := by gcongr
+  · calc
+      A ^ m ∩ B ^ n ⊆ (F₁ ^ (m - 1) * A) ∩ (F₂ ^ (n - 1) * B) := by
+        gcongr <;> apply pow_subset_pow_mul_of_sq_subset_mul <;> assumption
+      _ = ⋃ (a ∈ F₁ ^ (m - 1)) (b ∈ F₂ ^ (n - 1)), a • A ∩ b • B := by
+        simp_rw [← smul_eq_mul, ← iUnion_smul_set, iUnion₂_inter_iUnion₂]; norm_cast
+      _ ⊆ ⋃ (a ∈ F₁ ^ (m - 1)) (b ∈ F₂ ^ (n - 1)), f a b • (A ^ 2 ∩ B ^ 2) := by gcongr; exact hf ..
+      _ = (Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) * (A ^ 2 ∩ B ^ 2) := by
+        rw [Finset.coe_image₂, ← smul_eq_mul, ← iUnion_smul_set, biUnion_image2]
+        simp_rw [Finset.mem_coe]
+
+open Set in
+@[to_additive]
+lemma pow_inter_pow (hA : IsApproximateSubgroup K A) (hB : IsApproximateSubgroup L B) (hm : 2 ≤ m)
+    (hn : 2 ≤ n) (hAB : (A ^ m ∩ B ^ n).Nonempty) :
+    IsApproximateSubgroup (K ^ (2 * m - 1) * L ^ (2 * n - 1)) (A ^ m ∩ B ^ n) where
+  nonempty := hAB
+  inv_eq_self := by simp_rw [inter_inv, ← inv_pow, hA.inv_eq_self, hB.inv_eq_self]
+  exists_sq_subset_mul := by
+    obtain ⟨F, hF, hABF⟩ := hA.exists_pow_inter_pow_subset hB hm hn
+    sorry
+
 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 Finset in
+open scoped RightActions in
+@[to_additive]
+lemma exists_isApproximateSubgroup_of_small_doubling [DecidableEq G] {A : Finset G}
+    (hA₀ : A.Nonempty) (hA : #(A ^ 2) ≤ K * #A) :
+    ∃ S ⊆ (A⁻¹ * A) ^ 2, IsApproximateSubgroup (2 ^ 12 * K ^ 36) (S : Set G) ∧
+      #S ≤ 16 * K ^ 12 * #A ∧ ∃ a ∈ A, #A / (2 * K) ≤ #(A ∩ S <• a) := by
+  have hK : 1 ≤ K := sorry
+  let S : Finset G := {g ∈ A⁻¹ * A | #A / (2 * K) ≤ #(A <• g ∩ A)}
+  have hS₀ : S.Nonempty := ⟨1, by simp [S, hA₀.ne_empty]; bound⟩
+  have hSA : S ⊆ A⁻¹ * A := filter_subset ..
+  have hSsymm : S⁻¹ = S := by ext; simp [S]; simp [← mem_inv']; sorry
+  have hScard :=
+    calc
+      (#S : ℝ) ≤ #(A⁻¹ * A) := by gcongr
+      _ ≤ K ^ 2 * #A := sorry
+  refine ⟨S ^ 2, by gcongr, ⟨sorry, sorry, sorry⟩, ?_, ?_⟩
+  sorry
+  sorry

LeanCamCombi/GrowthInGroups/Lecture2.lean

@@ -33,7 +33,7 @@ lemma lemma_4_3_1 (hA : #(A ^ 2) ≤ K * #A) : #(A * A⁻¹) ≤ K ^ 2 * #A := b
 
 lemma lemma_4_4_1 (hm : 3 ≤ m) (hA : #(A ^ 3) ≤ K * #A) (ε : Fin m → ℤ) (hε : ∀ i, |ε i| = 1) :
     #((finRange m).map fun i ↦ A ^ ε i).prod ≤ K ^ (3 * (m - 2)) * #A :=
- small_alternating_pow_of_small_tripling' hm hA ε hε
+  small_alternating_pow_of_small_tripling' hm hA ε hε
 
 lemma lemma_4_4_2 (hm : 3 ≤ m) (hA : #(A ^ 3) ≤ K * #A) (hAsymm : A⁻¹ = A) :
     #(A ^ m) ≤ K ^ (m - 2) * #A := small_pow_of_small_tripling' hm hA hAsymm

LeanCamCombi/GrowthInGroups/Lecture3.lean

@@ -5,12 +5,36 @@ open Fin Finset List
 open scoped Pointwise
 
 namespace GrowthInGroups.Lecture3
-variable {G : Type*} [DecidableEq G] [Group G] {A : Finset G} {k K : ℝ} {m : ℕ}
+variable {G H : Type*} [Group G] [Group H] {A B : Set G} {K L : ℝ} {m n : ℕ}
 
-lemma lemma_5_1 {A : Finset G} (hA₀ : A.Nonempty) (hAsymm : A⁻¹ = A) (hA : #(A ^ 3) ≤ K * #A) :
-    IsApproximateSubgroup (A ^ 2 : Set G) (K ^ 3) := .of_small_tripling hA₀ hAsymm hA
+lemma lemma_5_1 [DecidableEq G] {A : Finset G} (hA₀ : A.Nonempty) (hAsymm : A⁻¹ = A)
+    (hA : #(A ^ 3) ≤ K * #A) : IsApproximateSubgroup (K ^ 3) (A ^ 2 : Set G) :=
+  .of_small_tripling hA₀ hAsymm hA
 
-lemma lemma_5_2 {A B : Finset G} (hB : B.Nonempty) (hK : #(A * B) ≤ K * #B) :
+lemma lemma_5_2 [DecidableEq G] {A B : Finset G} (hB : B.Nonempty) (hK : #(A * B) ≤ K * #B) :
     ∃ F ⊆ A, #F ≤ K ∧ A ⊆ F * B / B := ruzsa_covering_mul hB hK
 
+open scoped RightActions
+lemma proposition_5_3 [DecidableEq G] {A : Finset G} (hA₀ : A.Nonempty) (hA : #(A ^ 2) ≤ K * #A) :
+    ∃ S ⊆ (A⁻¹ * A) ^ 2, IsApproximateSubgroup (2 ^ 12 * K ^ 36) (S : Set G) ∧
+      #S ≤ 16 * K ^ 12 * #A ∧ ∃ a ∈ A, #A / (2 * K) ≤ #(A ∩ S <• a) :=
+  exists_isApproximateSubgroup_of_small_doubling hA₀ hA
+
+lemma fact_5_5 {A : Set G} (hA : IsApproximateSubgroup K A) (π : G →* H) :
+    IsApproximateSubgroup K (π '' A) := hA.image π
+
+lemma proposition_5_6_1 (hA : IsApproximateSubgroup K A) (hB : IsApproximateSubgroup L B)
+    (hm : 2 ≤ m) (hn : 2 ≤ n) :
+    ∃ F : Finset G, #F ≤ K ^ (m - 1) * L ^ (n - 1) ∧ A ^ m ∩ B ^ n ⊆ F * (A ^ 2 ∩ B ^ 2) :=
+  hA.exists_pow_inter_pow_subset hB hm hn
+
+lemma proposition_5_6_2 (hA : IsApproximateSubgroup K A) (hB : IsApproximateSubgroup L B)
+    (hm : 2 ≤ m) (hn : 2 ≤ n) (hAB : (A ^ m ∩ B ^ n).Nonempty) :
+    IsApproximateSubgroup (K ^ (2 * m - 1) * L ^ (2 * n - 1)) (A ^ m ∩ B ^ n) :=
+  hA.pow_inter_pow hB hm hn hAB
+
+lemma lemma_5_7 (hA : A⁻¹ = A) (hB : B⁻¹ = B) (x y : G) :
+    ∃ z : G, x • A ∩ y • B ⊆ z • (A ^ 2 ∩ B ^ 2) :=
+  Set.exists_smul_inter_smul_subset_smul_sq_inter_sq hA hB x y
+
 end GrowthInGroups.Lecture3

LeanCamCombi/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean

@@ -12,10 +12,10 @@ attribute [gcongr] mul_subset_mul_left mul_subset_mul_right div_subset_div_left
 end Finset
 
 namespace Finset
-variable {α : Type*} [DecidableEq α]
+variable {F α β : Type*} [DecidableEq α] [DecidableEq β]
 
 section Monoid
-variable [Monoid α] {s t : Finset α} {n : ℕ}
+variable [Monoid α] [Monoid β] {s t : Finset α} {n : ℕ}
 
 attribute [simp] one_nonempty
 
@@ -50,6 +50,37 @@ lemma pow_subset_pow_mul_of_sq_subset_mul (hst : s ^ 2 ⊆ t * s) :
       _ ⊆ t ^ (n + 1) * (t * s) := by gcongr
       _ = t ^ (n + 2) * s := by rw [← mul_assoc, ← pow_succ]
 
+@[to_additive]
+lemma pow_right_mono (hs : 1 ∈ s) : Monotone (s ^ ·) := by
+  apply monotone_nat_of_le_succ
+  intro n
+  rw [pow_succ]
+  exact subset_mul_left _ hs
+
+@[to_additive (attr := gcongr)]
+lemma pow_subset_pow_right (hs : 1 ∈ s) {m n : ℕ} (hmn : m ≤ n) : s ^ m ⊆ s ^ n :=
+  pow_right_mono hs hmn
+
+-- TODO: Replace `pow_subset_pow`
+@[to_additive (attr := gcongr)]
+lemma pow_subset_pow_left (hst : s ⊆ t) : ∀ {n : ℕ}, s ^ n ⊆ t ^ n
+  | 0 => by simp
+  | n + 1 => by simp_rw [pow_succ]; gcongr; exact pow_subset_pow_left hst
+
+@[to_additive]
+lemma pow_left_mono : Monotone fun s : Finset α ↦ s ^ n := fun _s _t hst ↦ pow_subset_pow_left hst
+
+-- TODO: Replace `pow_subset_pow`
+@[to_additive (attr := gcongr)]
+lemma pow_subset_pow' (hst : s ⊆ t) (ht : 1 ∈ t) {m n : ℕ} (hmn : m ≤ n) : s ^ m ⊆ t ^ n :=
+  (pow_left_mono hst).trans (pow_subset_pow_right ht hmn)
+
+@[to_additive]
+lemma image_pow [FunLike F α β] [MonoidHomClass F α β] (f : F) (s : Finset α) :
+    ∀ n, (s ^ n).image f = s.image f ^ n
+  | 0 => by simp [singleton_one]
+  | n + 1 => by simp [image_mul, pow_succ, image_pow]
+
 end Monoid
 
 section DivisionMonoid
@@ -72,4 +103,17 @@ set_option push_neg.use_distrib true in
     exact empty_zpow hn
 
 end DivisionMonoid
+
+section Group
+variable [Group α] {s t : Finset α}
+
+@[to_additive (attr := simp)]
+lemma one_mem_inv_mul_iff : (1 : α) ∈ t⁻¹ * s ↔ ¬Disjoint s t := by
+  aesop (add simp [not_disjoint_iff_nonempty_inter, mem_mul, mul_eq_one_iff_eq_inv,
+    Finset.Nonempty])
+
+@[to_additive]
+lemma not_one_mem_inv_mul_iff : (1 : α) ∉ t⁻¹ * s ↔ Disjoint s t := one_mem_inv_mul_iff.not_left
+
+end Group
 end Finset