Small tripling implies approximate subgroup

Author: YaelDillies

LeanCamCombi.lean

@@ -31,6 +31,8 @@ import LeanCamCombi.Mathlib.Analysis.Convex.Exposed
 import LeanCamCombi.Mathlib.Analysis.Convex.Extreme
 import LeanCamCombi.Mathlib.Analysis.Convex.Independence
 import LeanCamCombi.Mathlib.Analysis.Convex.SimplicialComplex.Basic
+import LeanCamCombi.Mathlib.Combinatorics.Additive.RuzsaCovering
+import LeanCamCombi.Mathlib.Combinatorics.Additive.SmallTripling
 import LeanCamCombi.Mathlib.Combinatorics.Schnirelmann
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Basic
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Containment

LeanCamCombi/GrowthInGroups/ApproximateSubgroup.lean

@@ -1,14 +1,12 @@
-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.Finset.Basic
 import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.Basic
+import LeanCamCombi.Mathlib.Combinatorics.Additive.RuzsaCovering
+import LeanCamCombi.Mathlib.Combinatorics.Additive.SmallTripling
+import LeanCamCombi.Mathlib.Data.Finset.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
@@ -65,14 +63,18 @@ lemma pi {ι : Type*} {G : ι → Type*} [Fintype ι] [∀ i, Group (G i)] {S :
         _ ≤ ∏ i, K i := by gcongr; exact hF _
     · sorry
 
+open Finset in
 @[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]
+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
+  nonempty := hA₀.to_set.pow
+  inv_eq_self := by simp [← inv_pow, hAsymm, ← coe_inv]
   exists_sq_subset_mul := by
-    sorry
-
-
+    replace hA := calc (#(A ^ 4 * A) : ℝ)
+      _ = #(A ^ 5) := by rw [← pow_succ]
+      _ ≤ K ^ 3 * #A := small_pow_of_small_tripling' (by omega) hA hAsymm
+    obtain ⟨F, -, hF, hAF⟩ := ruzsa_covering_mul hA₀ hA
+    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⟩
 
 end IsApproximateSubgroup

LeanCamCombi/GrowthInGroups/Lecture2.lean

@@ -1,4 +1,3 @@
-import Mathlib.Combinatorics.Additive.SmallTripling
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.Interval
 import LeanCamCombi.GrowthInGroups.ApproximateSubgroup
 
@@ -34,10 +33,10 @@ 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
+    #(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
 
@@ -63,11 +62,9 @@ lemma remark_4_6_3 : IsApproximateAddSubgroup (.Icc (-1) 1 : Set ℝ) 2 where
   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
+    IsApproximateSubgroup (A ^ 2 : Set G) (K ^ 3) := .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 _
+lemma lemma_4_8 {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
 
 end GrowthInGroups.Lecture2

LeanCamCombi/GrowthInGroups/Lecture3.lean

@@ -7,12 +7,10 @@ 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
+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
 
--- 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 _
+lemma lemma_5_2 {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
 
 end GrowthInGroups.Lecture3

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

@@ -12,7 +12,10 @@ attribute [gcongr] mul_subset_mul_left mul_subset_mul_right div_subset_div_left
 end Finset
 
 namespace Finset
-variable {α : Type*} [DecidableEq α] [Monoid α] {s t : Finset α}
+variable {α : Type*} [DecidableEq α]
+
+section Monoid
+variable [Monoid α] {s t : Finset α} {n : ℕ}
 
 attribute [simp] one_nonempty
 
@@ -21,6 +24,20 @@ lemma Nonempty.pow (hs : s.Nonempty) : ∀ {n}, (s ^ n).Nonempty
   | 0 => by simp
   | n + 1 => by rw [pow_succ]; exact hs.pow.mul hs
 
+set_option push_neg.use_distrib true in
+@[to_additive (attr := simp)] lemma pow_eq_empty : s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0 := by
+  constructor
+  · contrapose!
+    rintro (hs | rfl)
+    -- TODO: The `nonempty_iff_ne_empty` would be unnecessary if `push_neg` knew how to simplify
+    -- `s ≠ ∅` to `s.Nonempty` when `s : Finset α`.
+    -- See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/push_neg.20extensibility
+    · exact nonempty_iff_ne_empty.1 (nonempty_iff_ne_empty.2 hs).pow
+    · rw [← nonempty_iff_ne_empty]
+      simp
+  · rintro ⟨rfl, hn⟩
+    exact empty_pow hn
+
 @[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
@@ -33,4 +50,26 @@ 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]
 
+end Monoid
+
+section DivisionMonoid
+variable [DivisionMonoid α] {s t : Finset α} {n : ℤ}
+
+@[to_additive]
+lemma Nonempty.zpow (hs : s.Nonempty) : ∀ {n : ℤ}, (s ^ n).Nonempty
+  | (n : ℕ) => hs.pow
+  | .negSucc n => by simpa using hs.pow
+
+set_option push_neg.use_distrib true in
+@[to_additive (attr := simp)] lemma zpow_eq_empty : s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0 := by
+  constructor
+  · contrapose!
+    rintro (hs | rfl)
+    · exact nonempty_iff_ne_empty.1 (nonempty_iff_ne_empty.2 hs).zpow
+    · rw [← nonempty_iff_ne_empty]
+      simp
+  · rintro ⟨rfl, hn⟩
+    exact empty_zpow hn
+
+end DivisionMonoid
 end Finset

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

@@ -3,7 +3,10 @@ import Mathlib.Algebra.Group.Pointwise.Set.Basic
 open scoped Pointwise
 
 namespace Set
-variable {α : Type*} [Monoid α] {s t : Set α}
+variable {α : Type*}
+
+section Monoid
+variable [Monoid α] {s t : Set α} {n : ℕ}
 
 attribute [simp] one_nonempty
 
@@ -12,6 +15,16 @@ lemma Nonempty.pow (hs : s.Nonempty) : ∀ {n}, (s ^ n).Nonempty
   | 0 => by simp
   | n + 1 => by rw [pow_succ]; exact hs.pow.mul hs
 
+set_option push_neg.use_distrib true in
+@[to_additive (attr := simp)] lemma pow_eq_empty : s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0 := by
+  constructor
+  · contrapose!
+    rintro (hs | rfl)
+    · exact hs.pow
+    · simp
+  · rintro ⟨rfl, hn⟩
+    exact empty_pow hn
+
 @[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
@@ -24,6 +37,27 @@ 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]
 
+end Monoid
+
+section DivisionMonoid
+variable [DivisionMonoid α] {s t : Set α} {n : ℤ}
+
+@[to_additive]
+lemma Nonempty.zpow (hs : s.Nonempty) : ∀ {n : ℤ}, (s ^ n).Nonempty
+  | (n : ℕ) => hs.pow
+  | .negSucc n => by simpa using hs.pow
+
+set_option push_neg.use_distrib true in
+@[to_additive (attr := simp)] lemma zpow_eq_empty : s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0 := by
+  constructor
+  · contrapose!
+    rintro (hs | rfl)
+    · exact hs.zpow
+    · simp
+  · rintro ⟨rfl, hn⟩
+    exact empty_zpow hn
+
+end DivisionMonoid
 end Set
 
 namespace Set

LeanCamCombi/Mathlib/Combinatorics/Additive/RuzsaCovering.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2022 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import Mathlib.Data.Real.Basic
+import Mathlib.SetTheory.Cardinal.Finite
+import Mathlib.Tactic.Positivity.Finset
+import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
+
+/-!
+# Ruzsa's covering lemma
+
+This file proves the Ruzsa covering lemma. This says that, for `A`, `B` finsets, we can cover `A`
+with at most `#(A + B) / #B` copies of `B - B`.
+-/
+
+open scoped Pointwise
+
+variable {G : Type*} [Group G] {K : ℝ}
+
+namespace Finset
+variable [DecidableEq G] {A B : Finset G}
+
+/-- **Ruzsa's covering lemma**. -/
+@[to_additive "**Ruzsa's covering lemma**"]
+theorem ruzsa_covering_mul (hB : B.Nonempty) (hK : #(A * B) ≤ K * #B) :
+    ∃ F ⊆ A, #F ≤ K ∧ A ⊆ F * B / B := by
+  haveI : ∀ F, Decidable ((F : Set G).PairwiseDisjoint (· • B)) := fun F ↦ Classical.dec _
+  set C := {F ∈ A.powerset | F.toSet.PairwiseDisjoint (· • B)}
+  obtain ⟨F, hF, hFmax⟩ := C.exists_maximal <| filter_nonempty_iff.2
+    ⟨∅, empty_mem_powerset _, by rw [coe_empty]; exact Set.pairwiseDisjoint_empty⟩
+  rw [mem_filter, mem_powerset] at hF
+  obtain ⟨hFA, hF⟩ := hF
+  refine ⟨F, hFA, le_of_mul_le_mul_right ?_ (by positivity : (0 : ℝ) < #B), fun a ha ↦ ?_⟩
+  · calc
+      (#F * #B : ℝ) = #(F * B) := by
+        rw [card_mul_iff.2 <| pairwiseDisjoint_smul_iff.1 hF, Nat.cast_mul]
+      _ ≤ #(A * B) := by gcongr
+      _ ≤ K * #B := hK
+  rw [mul_div_assoc]
+  by_cases hau : a ∈ F
+  · exact subset_mul_left _ hB.one_mem_div hau
+  by_cases H : ∀ b ∈ F, Disjoint (a • B) (b • B)
+  · refine (hFmax _ ?_ <| ssubset_insert hau).elim
+    rw [mem_filter, mem_powerset, insert_subset_iff, coe_insert]
+    exact ⟨⟨ha, hFA⟩, hF.insert fun _ hb _ ↦ H _ hb⟩
+  push_neg at H
+  simp_rw [not_disjoint_iff, ← inv_smul_mem_iff] at H
+  obtain ⟨b, hb, c, hc₁, hc₂⟩ := H
+  exact mem_mul.2 ⟨b, hb, b⁻¹ * a, mem_div.2 ⟨_, hc₂, _, hc₁, by simp⟩, by simp⟩
+
+end Finset
+
+namespace Set
+variable {A B : Set G}
+
+/-- **Ruzsa's covering lemma** for sets. See also `Finset.exists_subset_mul_div`. -/
+@[to_additive "**Ruzsa's covering lemma** for sets. See also `Finset.exists_subset_add_sub`"]
+lemma ruzsa_covering_mul (hA : A.Finite) (hB : B.Finite) (hB₀ : B.Nonempty)
+    (hK : Nat.card (A * B) ≤ K * Nat.card B) :
+    ∃ F ⊆ A, Nat.card F ≤ K ∧ A ⊆ F * B / B ∧ F.Finite := by
+  lift A to Finset G using hA
+  lift B to Finset G using hB
+  classical
+  obtain ⟨F, hFA, hF, hAF⟩ := Finset.ruzsa_covering_mul hB₀ (by simpa [← Finset.coe_mul] using hK)
+  exact ⟨F, by norm_cast; simp [*]⟩
+
+end Set