GrowthInGroups: Cover by translates relation

Author: YaelDillies

LeanCamCombi.lean

@@ -21,6 +21,7 @@ import LeanCamCombi.GrowthInGroups.Lecture2
 import LeanCamCombi.GrowthInGroups.Lecture3
 import LeanCamCombi.GrowthInGroups.PolynomialLocalization
 import LeanCamCombi.GrowthInGroups.PrimeSpectrumPolynomial
+import LeanCamCombi.GrowthInGroups.SMulCover
 import LeanCamCombi.GrowthInGroups.VerySmallDoubling
 import LeanCamCombi.Impact
 import LeanCamCombi.Incidence
@@ -56,8 +57,11 @@ import LeanCamCombi.Mathlib.Data.Finset.PosDiffs
 import LeanCamCombi.Mathlib.Data.Fintype.Card
 import LeanCamCombi.Mathlib.Data.List.DropRight
 import LeanCamCombi.Mathlib.Data.Multiset.Basic
+import LeanCamCombi.Mathlib.Data.Nat.Cast.Order.Basic
 import LeanCamCombi.Mathlib.Data.Prod.Lex
+import LeanCamCombi.Mathlib.Data.Set.Basic
 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

LeanCamCombi/GrowthInGroups/ApproximateSubgroup.lean

@@ -1,14 +1,13 @@
 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
+import LeanCamCombi.GrowthInGroups.SMulCover
 
 -- TODO: Unsimp in mathlib
 attribute [-simp] Set.image_subset_iff
@@ -20,35 +19,35 @@ variable {G : Type*} [Group G] {A B : Set G} {K L : ℝ} {m n : ℕ}
 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
+  two_nsmul_vaddCovered : VAddCovered G K (2 • A) A
 
 @[to_additive]
 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
+  sq_smulCovered : SMulCovered G K (A ^ 2) A
 
 namespace IsApproximateSubgroup
 
 @[to_additive one_le]
 lemma one_le (hA : IsApproximateSubgroup K A) : 1 ≤ K := by
-  obtain ⟨F, hF, hSF⟩ := hA.exists_sq_subset_mul
+  obtain ⟨F, hF, hSF⟩ := hA.sq_smulCovered
   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) (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⟩
+  sq_smulCovered := hA.sq_smulCovered.mono hKL
 
 @[to_additive]
 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⟩ := hA.exists_sq_subset_mul
+    obtain ⟨F, hF, hSF⟩ := hA.sq_smulCovered
     calc
       (#(A ^ (n + 2)) : ℝ) ≤ #(F ^ (n + 1) * A) := by
         gcongr; exact mod_cast Set.pow_subset_pow_mul_of_sq_subset_mul hSF (by omega)
@@ -61,14 +60,14 @@ lemma image {F H : Type*} [Group H] [FunLike F G H] [MonoidHomClass F G H] (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
+  sq_smulCovered := by
     classical
-    obtain ⟨F, hF, hAF⟩ := hA.exists_sq_subset_mul
+    obtain ⟨F, hF, hAF⟩ := hA.sq_smulCovered
     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]
+    · simp only [← Set.image_pow, Finset.coe_image, ← Set.image_mul, smul_eq_mul] at hAF ⊢
       gcongr
 
 @[to_additive]
@@ -77,8 +76,8 @@ lemma pi {ι : Type*} {G : ι → Type*} [Fintype ι] [∀ i, Group (G i)] {A :
     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
+  sq_smulCovered := by
+    choose F hF hFS using fun i ↦ (hA i).sq_smulCovered
     classical
     refine ⟨Fintype.piFinset F, ?_, ?_⟩
     · calc
@@ -91,15 +90,15 @@ 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⟩
+  sq_smulCovered := ⟨{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 (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
+  sq_smulCovered := by
     replace hA := calc (#(A ^ 4 * A) : ℝ)
       _ = #(A ^ 5) := by rw [← pow_succ]
       _ ≤ K ^ 3 * #A := small_pow_of_small_tripling' (by omega) hA hAsymm
@@ -113,8 +112,8 @@ lemma exists_pow_inter_pow_subset (hA : IsApproximateSubgroup K A) (hB : IsAppro
     (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
+  obtain ⟨F₁, hF₁, hAF₁⟩ := hA.sq_smulCovered
+  obtain ⟨F₂, hF₂, hBF₂⟩ := hB.sq_smulCovered
   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)), ?_, ?_⟩
@@ -140,7 +139,7 @@ lemma pow_inter_pow (hA : IsApproximateSubgroup K A) (hB : IsApproximateSubgroup
     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
+  sq_smulCovered := by
     obtain ⟨F, hF, hABF⟩ := hA.exists_pow_inter_pow_subset hB hm hn
     sorry
 

LeanCamCombi/GrowthInGroups/Lecture2.lean

@@ -38,31 +38,31 @@ lemma lemma_4_4_1 (hm : 3 ≤ m) (hA : #(A ^ 3) ≤ K * #A) (ε : Fin m → ℤ)
 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
+def def_4_5 (S : Set G) (K : ℝ) : Prop := IsApproximateSubgroup K S
 
 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
+lemma remark_4_6_1 (k : ℕ) : IsApproximateAddSubgroup 2 (.Icc (-k) k : Set ℤ) where
   nonempty := ⟨0, by simp⟩
   neg_eq_self := by simp
-  exists_two_nsmul_subset_add :=
+  two_nsmul_vaddCovered :=
     ⟨{(-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
+    IsApproximateAddSubgroup (2 ^ Fintype.card ι)
+      (Set.univ.pi fun i ↦ .Icc (-k i) (k i) : Set (ι → ℤ)) := 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
+lemma remark_4_6_3 : IsApproximateAddSubgroup 2 (.Icc (-1) 1 : Set ℝ) 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]⟩
+  two_nsmul_vaddCovered := ⟨{-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 ^ 3) := .of_small_tripling hA₀ hsymm hA
+    IsApproximateSubgroup (K ^ 3) (A ^ 2 : Set G) := .of_small_tripling hA₀ hsymm hA
 
 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

LeanCamCombi/GrowthInGroups/SMulCover.lean

@@ -0,0 +1,43 @@
+import Mathlib.Data.Real.Basic
+import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
+import LeanCamCombi.Mathlib.Data.Nat.Cast.Order.Basic
+
+open scoped Finset Pointwise
+
+variable {M N X : Type*} [Monoid M] [Monoid N] [MulAction M X] [MulAction N X] {K L : ℝ}
+  {A B C : Set X}
+
+variable (M) in
+@[to_additive] def SMulCovered (K : ℝ) (A B : Set X) : Prop :=
+  ∃ F : Finset M, #F ≤ K ∧ A ⊆ (F : Set M) • B
+
+@[to_additive (attr := simp, refl)]
+lemma SMulCovered.rfl : SMulCovered M 1 A A := ⟨1, by simp⟩
+
+@[to_additive (attr := simp)]
+lemma SMulCovered.of_subset (hAB : A ⊆ B) : SMulCovered M 1 A B := ⟨1, by simpa⟩
+
+@[to_additive] lemma SMulCovered.nonneg : SMulCovered M K A B → 0 ≤ K := by
+  rintro ⟨F, hF, -⟩; exact (#F).cast_nonneg.trans hF
+
+@[to_additive (attr := simp)]
+lemma smulCovered_zero : SMulCovered M 0 A B ↔ A = ∅ := by simp [SMulCovered]
+
+@[to_additive]
+lemma SMulCovered.mono (hKL : K ≤ L) : SMulCovered M K A B → SMulCovered M L A B := by
+  rintro ⟨F, hF, hFAB⟩; exact ⟨F, hF.trans hKL, hFAB⟩
+
+@[to_additive] lemma SMulCovered.trans [MulAction M N] [IsScalarTower M N X]
+    (hAB : SMulCovered M K A B) (hBC : SMulCovered N L B C) : SMulCovered N (K * L) A C := by
+  classical
+  have := hAB.nonneg
+  obtain ⟨F₁, hF₁, hFAB⟩ := hAB
+  obtain ⟨F₂, hF₂, hFBC⟩ := hBC
+  refine ⟨F₁ • F₂, ?_, ?_⟩
+  · calc
+      (#(F₁ • F₂) : ℝ) ≤ #F₁ * #F₂ := mod_cast Finset.card_smul_le
+      _ ≤ K * L := by gcongr
+  · calc
+      A ⊆ (F₁ : Set M) • B := hFAB
+      _ ⊆ (F₁ : Set M) • (F₂ : Set N) • C := by gcongr
+      _ = (↑(F₁ • F₂) : Set N) • C := by simp

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 {F α β : Type*} [DecidableEq α] [DecidableEq β]
+variable {F α β : Type*}
 
 section Monoid
-variable [Monoid α] [Monoid β] {s t : Finset α} {n : ℕ}
+variable [DecidableEq α] [DecidableEq β] [Monoid α] [Monoid β] {s t : Finset α} {n : ℕ}
 
 attribute [simp] one_nonempty
 
@@ -84,7 +84,7 @@ lemma image_pow [FunLike F α β] [MonoidHomClass F α β] (f : F) (s : Finset 
 end Monoid
 
 section DivisionMonoid
-variable [DivisionMonoid α] {s t : Finset α} {n : ℤ}
+variable [DecidableEq α] [DivisionMonoid α] {s t : Finset α} {n : ℤ}
 
 @[to_additive]
 lemma Nonempty.zpow (hs : s.Nonempty) : ∀ {n : ℤ}, (s ^ n).Nonempty
@@ -105,7 +105,7 @@ set_option push_neg.use_distrib true in
 end DivisionMonoid
 
 section Group
-variable [Group α] {s t : Finset α}
+variable [DecidableEq α] [Group α] {s t : Finset α}
 
 @[to_additive (attr := simp)]
 lemma one_mem_inv_mul_iff : (1 : α) ∈ t⁻¹ * s ↔ ¬Disjoint s t := by
@@ -116,4 +116,11 @@ lemma one_mem_inv_mul_iff : (1 : α) ∈ t⁻¹ * s ↔ ¬Disjoint s t := by
 lemma not_one_mem_inv_mul_iff : (1 : α) ∉ t⁻¹ * s ↔ Disjoint s t := one_mem_inv_mul_iff.not_left
 
 end Group
+
+section MulAction
+variable [DecidableEq β] [Monoid α] [MulAction α β] {s : Finset α} {t : Finset β}
+
+@[to_additive] lemma card_smul_le : #(s • t) ≤ #s * #t := card_image₂_le ..
+
+end MulAction
 end Finset

LeanCamCombi/Mathlib/Algebra/Group/Subgroup/Pointwise.lean

@@ -24,6 +24,6 @@ variable {G S : Type*} [Group G] [SetLike S G] [SubgroupClass S G] {s : Set G} {
 
 set_option linter.unusedVariables false in
 @[to_additive (attr := simp)]
-lemma coe_pow : ∀ {n} (hn : n ≠ 0) (H : S), (H ^ n : Set G) = H
+lemma coe_set_pow : ∀ {n} (hn : n ≠ 0) (H : S), (H ^ n : Set G) = H
   | 1, _, H => by simp
-  | n + 2, _, H => by rw [pow_succ, coe_pow n.succ_ne_zero, coe_mul_coe]
+  | n + 2, _, H => by rw [pow_succ, coe_set_pow n.succ_ne_zero, coe_mul_coe]

LeanCamCombi/Mathlib/Data/Nat/Cast/Order/Basic.lean

@@ -0,0 +1,5 @@
+import Mathlib.Data.Nat.Cast.Order.Basic
+
+@[simp]
+lemma Nat.cast_nonpos {α : Type*} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α]
+    [ZeroLEOneClass α] [CharZero α] {n : ℕ} : (n : α) ≤ 0 ↔ n ≤ 0 := by norm_cast