Finish stating Lecture 2

Author: YaelDillies

LeanCamCombi.lean

@@ -10,11 +10,13 @@ import LeanCamCombi.ErdosRenyi.Connectivity
 import LeanCamCombi.ErdosRenyi.GiantComponent
 import LeanCamCombi.GraphTheory.ExampleSheet1
 import LeanCamCombi.GraphTheory.ExampleSheet2
+import LeanCamCombi.GrowthInGroups.ApproximateSubgroup
 import LeanCamCombi.GrowthInGroups.BooleanSubalgebra
 import LeanCamCombi.GrowthInGroups.Chevalley
 import LeanCamCombi.GrowthInGroups.Constructible
 import LeanCamCombi.GrowthInGroups.Lecture1
 import LeanCamCombi.GrowthInGroups.Lecture2
+import LeanCamCombi.GrowthInGroups.Lecture3
 import LeanCamCombi.GrowthInGroups.SmallTripling
 import LeanCamCombi.GrowthInGroups.VerySmallDoubling
 import LeanCamCombi.Impact
@@ -24,6 +26,7 @@ import LeanCamCombi.Kneser.KneserRuzsa
 import LeanCamCombi.Kneser.MulStab
 import LeanCamCombi.LittlewoodOfford
 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.Analysis.Convex.Exposed
 import LeanCamCombi.Mathlib.Analysis.Convex.Extreme
@@ -46,6 +49,7 @@ import LeanCamCombi.Mathlib.Data.Prod.Lex
 import LeanCamCombi.Mathlib.Data.Set.Image
 import LeanCamCombi.Mathlib.Data.Set.Lattice
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.Finite
+import LeanCamCombi.Mathlib.Data.Set.Pointwise.Interval
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
 import LeanCamCombi.Mathlib.GroupTheory.OrderOfElement
 import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

LeanCamCombi/GrowthInGroups/ApproximateSubgroup.lean

@@ -0,0 +1,78 @@
+import Mathlib.Algebra.BigOperators.Ring
+import Mathlib.Algebra.Group.Pointwise.Finset.Basic
+import Mathlib.Algebra.Order.BigOperators.Ring.Finset
+import Mathlib.Combinatorics.Additive.RuzsaCovering
+import Mathlib.Data.Fintype.BigOperators
+import Mathlib.Data.Real.Basic
+import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.Basic
+
+open scoped Finset Pointwise
+
+
+variable {G : Type*} [Group G] {S : Set G} {K L : ℝ} {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
+
+@[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
+
+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
+  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⟩
+
+@[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
+  | 1 => by simp
+  | n + 2 => by
+    obtain ⟨F, hF, hSF⟩ := hS.exists_sq_subset_mul
+    calc
+      (#(S ^ (n + 2)) : ℝ) ≤ #(F ^ (n + 1) * S) := 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
+
+@[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]
+  exists_sq_subset_mul := by
+    choose F hF hFS using fun i ↦ (hS 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 of_small_tripling [DecidableEq G] {s : Finset G} (hs₀ : s.Nonempty) (hsymm : s⁻¹ = s)
+    (hs : #(s ^ 3) ≤ K * #s) : IsApproximateSubgroup (s ^ 2 : Set G) (K ^ 2) where
+  nonempty := hs₀.to_set.pow
+  inv_eq_self := by simp [← inv_pow, hsymm, ← Finset.coe_inv]
+  exists_sq_subset_mul := by
+    sorry
+
+
+
+end IsApproximateSubgroup

LeanCamCombi/GrowthInGroups/Lecture2.lean

@@ -1,7 +1,5 @@
-import Mathlib.Data.Real.Basic
-import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic.FinCases
-import Mathlib.Tactic.NormNum
+import LeanCamCombi.Mathlib.Data.Set.Pointwise.Interval
+import LeanCamCombi.GrowthInGroups.ApproximateSubgroup
 import LeanCamCombi.GrowthInGroups.SmallTripling
 
 open Fin Finset List
@@ -10,7 +8,6 @@ open scoped Pointwise
 namespace GrowthInGroups.Lecture2
 variable {G : Type*} [DecidableEq G] [Group G] {A : Finset G} {k K : ℝ} {m : ℕ}
 
--- TODO: Genealise to non-commutative groups
 lemma lemma_4_2 (U V W : Finset G) : #U * #(V⁻¹ * W) ≤ #(U * V) * #(U * W) := by
   exact ruzsa_triangle_inequality_invMul_mul_mul ..
 
@@ -35,12 +32,42 @@ lemma lemma_4_3_1 (hA : #(A ^ 2) ≤ K * #A) : #(A * A⁻¹) ≤ K ^ 2 * #A := b
     _ ≤ (K * #A) * (K * #A) := by rw [← sq A]; gcongr
     _ = #A * (K ^ 2 * #A) := by ring
 
-lemma lemma_4_4_1 (hm : 3 ≤ m) (hA : #(A ^ 3) ≤ K * #A) (ε : Fin m → ℤ)
-    (hε : ∀ i, |ε i| = 1) :
+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ε
 
 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
 
+def def_4_5 (S : Set G) (K : ℝ) : Prop := IsApproximateSubgroup S K
+
+lemma two_nsmul_Icc_nat (k : ℕ) : (2 • .Icc (-k) k : Set ℤ) = {(-k : ℤ), (k : ℤ)} + .Icc (-k) k :=
+  sorry
+
+lemma two_nsmul_Icc_real : (2 • .Icc (-1) 1 : Set ℝ) = {-1, 1} + .Icc (-1) 1 := sorry
+
+lemma remark_4_6_1 (k : ℕ) : IsApproximateAddSubgroup (.Icc (-k) k : Set ℤ) 2 where
+  nonempty := ⟨0, by simp⟩
+  neg_eq_self := by simp
+  exists_two_nsmul_subset_add :=
+    ⟨{(-k : ℤ), (k : ℤ)}, mod_cast card_le_two, by simp [two_nsmul_Icc_nat]⟩
+
+lemma remark_4_6_2 {ι : Type*} [Fintype ι] (k : ι → ℕ) :
+    IsApproximateAddSubgroup (Set.univ.pi fun i ↦ .Icc (-k i) (k i) : Set (ι → ℤ))
+      (2 ^ Fintype.card ι) := by
+  simpa using IsApproximateAddSubgroup.pi fun i ↦ remark_4_6_1 (k i)
+
+lemma remark_4_6_3 : IsApproximateAddSubgroup (.Icc (-1) 1 : Set ℝ) 2 where
+  nonempty := ⟨0, by simp⟩
+  neg_eq_self := by simp
+  exists_two_nsmul_subset_add := ⟨{-1, 1}, mod_cast card_le_two, by simp [two_nsmul_Icc_real]⟩
+
+lemma lemma_4_7 {A : Finset G} (hA₀ : A.Nonempty) (hsymm : A⁻¹ = A) (hA : #(A ^ 3) ≤ K * #A) :
+    IsApproximateSubgroup (A ^ 2 : Set G) (K ^ 2) := .of_small_tripling hA₀ hsymm hA
+
+-- TODO: Generalise Ruzsa covering to non-abelian groups
+lemma lemma_4_8 {A B : Finset G} (hK : #(A * B) ≤ K * #B) : ∃ F ⊆ A, #F ≤ K ∧ A ⊆ F * (B / B) := by
+  sorry
+  -- obtain ⟨F, hF⟩ := Finset.exists_subset_mul_div A _
+
 end GrowthInGroups.Lecture2

LeanCamCombi/GrowthInGroups/Lecture3.lean

@@ -0,0 +1,19 @@
+import LeanCamCombi.Mathlib.Data.Set.Pointwise.Interval
+import LeanCamCombi.GrowthInGroups.ApproximateSubgroup
+import LeanCamCombi.GrowthInGroups.SmallTripling
+
+open Fin Finset List
+open scoped Pointwise
+
+namespace GrowthInGroups.Lecture3
+variable {G : Type*} [DecidableEq G] [Group G] {A : Finset G} {k K : ℝ} {m : ℕ}
+
+lemma lemma_5_1 {A : Finset G} (hA₀ : A.Nonempty) (hsymm : A⁻¹ = A) (hA : #(A ^ 3) ≤ K * #A) :
+    IsApproximateSubgroup (A ^ 2 : Set G) (K ^ 2) := .of_small_tripling hA₀ hsymm hA
+
+-- TODO: Generalise Ruzsa covering to non-abelian groups
+lemma lemma_5_2 {A B : Finset G} (hK : #(A * B) ≤ K * #B) : ∃ F ⊆ A, #F ≤ K ∧ A ⊆ F * (B / B) := by
+  sorry
+  -- obtain ⟨F, hF⟩ := Finset.exists_subset_mul_div A _
+
+end GrowthInGroups.Lecture3

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

@@ -7,4 +7,30 @@ variable {α : Type*} [DecidableEq α] [Mul α] {s t : Finset α} {a : α}
 
 lemma smul_finset_subset_mul : a ∈ s → a • t ⊆ s * t := image_subset_image₂_right
 
+attribute [gcongr] mul_subset_mul_left mul_subset_mul_right div_subset_div_left div_subset_div_right
+
+end Finset
+
+namespace Finset
+variable {α : Type*} [DecidableEq α] [Monoid α] {s t : Finset α}
+
+attribute [simp] one_nonempty
+
+@[to_additive]
+lemma Nonempty.pow (hs : s.Nonempty) : ∀ {n}, (s ^ n).Nonempty
+  | 0 => by simp
+  | n + 1 => by rw [pow_succ]; exact hs.pow.mul hs
+
+@[to_additive]
+lemma pow_subset_pow_mul_of_sq_subset_mul (hst : s ^ 2 ⊆ t * s) :
+    ∀ {n}, 1 < n → s ^ n ⊆ t ^ (n - 1) * s
+  | 2, _ => by simpa
+  | n + 3, _ => by
+    calc
+      s ^ (n + 3) = s ^ (n + 2) * s := by rw [pow_succ]
+      _ ⊆ t ^ (n + 1) * s * s := by gcongr; exact pow_subset_pow_mul_of_sq_subset_mul hst (by omega)
+      _ = t ^ (n + 1) * s ^ 2 := by rw [mul_assoc, sq]
+      _ ⊆ t ^ (n + 1) * (t * s) := by gcongr
+      _ = t ^ (n + 2) * s := by rw [← mul_assoc, ← pow_succ]
+
 end Finset

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

@@ -0,0 +1,36 @@
+import Mathlib.Algebra.Group.Pointwise.Set.Basic
+
+open scoped Pointwise
+
+namespace Set
+variable {α : Type*} [Monoid α] {s t : Set α}
+
+attribute [simp] one_nonempty
+
+@[to_additive]
+lemma Nonempty.pow (hs : s.Nonempty) : ∀ {n}, (s ^ n).Nonempty
+  | 0 => by simp
+  | n + 1 => by rw [pow_succ]; exact hs.pow.mul hs
+
+@[to_additive]
+lemma pow_subset_pow_mul_of_sq_subset_mul (hst : s ^ 2 ⊆ t * s) :
+    ∀ {n}, 1 < n → s ^ n ⊆ t ^ (n - 1) * s
+  | 2, _ => by simpa
+  | n + 3, _ => by
+    calc
+      s ^ (n + 3) = s ^ (n + 2) * s := by rw [pow_succ]
+      _ ⊆ t ^ (n + 1) * s * s := by gcongr; exact pow_subset_pow_mul_of_sq_subset_mul hst (by omega)
+      _ = t ^ (n + 1) * s ^ 2 := by rw [mul_assoc, sq]
+      _ ⊆ t ^ (n + 1) * (t * s) := by gcongr
+      _ = t ^ (n + 2) * s := by rw [← mul_assoc, ← pow_succ]
+
+end Set
+
+namespace Set
+variable {ι : Type*} {α : ι → Type*} [∀ i, InvolutiveInv (α i)]
+
+@[to_additive (attr := simp)]
+lemma inv_pi (s : Set ι) (t : ∀ i, Set (α i)) : (s.pi t)⁻¹ = s.pi fun i ↦ (t i)⁻¹ := by
+  simp_rw [← image_inv]; exact piMap_image_pi (fun _ _ ↦ inv_surjective) _
+
+end Set

LeanCamCombi/Mathlib/Data/Set/Pointwise/Interval.lean

@@ -0,0 +1,11 @@
+import Mathlib.Data.Set.Pointwise.Interval
+
+open scoped Pointwise
+
+namespace Set
+variable {α : Type*} [OrderedCommGroup α]
+
+@[to_additive (attr := simp)]
+lemma inv_Icc (a b : α) : (Icc a b)⁻¹ = Icc b⁻¹ a⁻¹ := by ext; simp [le_inv', inv_le', and_comm]
+
+end Set