Knester Ruzsa progress (#12)

This PR proves the reduction to the quotient group in Lemma 3.3 (in Ruzsa's notes). Some further partial progress is made and some inaccuracies in the proof sketch are noted
YaelDillies · Dec 22, 2023 · 47bad1c · 47bad1c
1 parent 9791f35
commit 47bad1c
Show file tree

Hide file tree

Showing 3 changed files with 184 additions and 14 deletions.
diff --git a/LeanCamCombi/Kneser/KneserRuzsa.lean b/LeanCamCombi/Kneser/KneserRuzsa.lean
@@ -27,16 +27,17 @@ if the inequality is strict, then we in fact have `|s + H| + |t + H| ≤ |s + t|
 * Matt DeVos, *A short proof of Kneser's addition lemma*
 -/
 
-open Function MulAction
+open Function MulAction Subgroup
 
 open scoped Classical Pointwise
 
-variable {ι α : Type*} [CommGroup α] [DecidableEq α] {s s' t t' C : Finset α} {a b : α}
+variable {α : Type*} [CommGroup α] [DecidableEq α] {s t : Finset α}
 
 namespace Finset
 
 /-! ### Auxiliary results -/
 
+
 -- Lemma 3.3 in Ruzsa's notes
 @[to_additive]
 lemma le_card_union_add_card_mulStab_union :
@@ -46,23 +47,110 @@ lemma le_card_union_add_card_mulStab_union :
   -- TODO: `to_additive` chokes on `zero_le'`
   obtain rfl | ht := t.eq_empty_or_nonempty
   · simp [-zero_le']
-  obtain hst | hst := (subset_union_left s t).eq_or_ssubset
-  · simp [hst.symm]
-  obtain hts | hts := (subset_union_right s t).eq_or_ssubset
-  · simp [hts.symm]
   set Hs := s.mulStab with hHs
   set Ht := t.mulStab with hHt
   set H := Hs * Ht with hH
   have hHs : Hs.Nonempty := hs.mulStab
   have hHt : Ht.Nonempty := ht.mulStab
   have hH : H.Nonempty := hHs.mul hHt
-  have : Hs ∩ Ht = 1 := by sorry
+  wlog h1: Hs ∩ Ht = 1
+  · set N := stabilizer α s ⊓ stabilizer α t with hN
+    have hNmulstab : (N : Set α) = ↑(Hs ∩ Ht) := by aesop
+    replace h1 : mulStab (image (QuotientGroup.mk (s := N)) s) ∩
+      mulStab (image QuotientGroup.mk t) = 1 := by
+      ext x
+      constructor
+      · simp only [Nonempty.image_iff, mem_one, and_imp, ← QuotientGroup.mk_one]
+        intro hx
+        rw [←  mul_stab_quotient_commute_subgroup N s,
+            ← mul_stab_quotient_commute_subgroup N t] at hx
+        simp only [mem_inter, mem_image] at hx
+        obtain ⟨⟨y, hy, hyx⟩, ⟨z, hz, hzx⟩⟩ := hx
+        obtain ⟨w, hwx⟩ := Quotient.exists_rep x
+        have : ⟦w⟧ = QuotientGroup.mk (s := N) w := by exact rfl
+        rw [← hwx, this, QuotientGroup.eq] at hyx hzx ⊢
+        simp only [mul_one, ge_iff_le, inv_mem_iff, mem_inf, mem_stabilizer_iff] at hyx hzx ⊢
+        constructor
+        · convert hyx.1 using 1
+          rw [mul_comm, mul_smul]
+          congr
+          simp only [← inv_smul_eq_iff, inv_inv, ← (mem_mulStab hs), hy]
+        · convert hzx.2 using 1
+          rw [mul_comm, mul_smul]
+          congr
+          simp only [← inv_smul_eq_iff, inv_inv, ← (mem_mulStab ht), hz]
+        all_goals { aesop }
+      · aesop
+    specialize this (α := α ⧸ N) (s := s.image (↑)) (t := t.image (↑))
+    simp only [Nonempty.image_iff, mulStab_nonempty, mul_nonempty, ge_iff_le, and_imp,
+      forall_true_left, hs, ht, h1] at this
+    calc
+    min (card s + card Hs) (card t + card Ht) =
+      min (Nat.card N * card (s.image (QuotientGroup.mk (s := N))) +
+      Nat.card N * card (Hs.image (QuotientGroup.mk (s := N))))
+      (Nat.card N * card (t.image (QuotientGroup.mk (s := N))) +
+      Nat.card N * card (Ht.image (QuotientGroup.mk (s := N)))) := by
+        rw [← subgroup_mul_card_eq_mul_of_mul_stab_subset N s,
+        ← subgroup_mul_card_eq_mul_of_mul_stab_subset N t,
+        ← subgroup_mul_card_eq_mul_of_mul_stab_subset N Hs,
+        ← subgroup_mul_card_eq_mul_of_mul_stab_subset N Ht]
+        all_goals { aesop }
+    _ = Nat.card N * min (card (s.image (QuotientGroup.mk (s := N))) +
+      card (Hs.image (QuotientGroup.mk (s := N)))) (card (t.image (QuotientGroup.mk (s := N))) +
+      card (Ht.image (QuotientGroup.mk (s := N)))) := by
+        rw [← mul_add, ← mul_add, Nat.mul_min_mul_left]
+    _ = Nat.card N * min (card (image (QuotientGroup.mk (s := N)) s) +
+      card (mulStab (image (QuotientGroup.mk (s := N)) s)))
+      (card (image (QuotientGroup.mk (s := N)) t) +
+      card (mulStab (image (QuotientGroup.mk (s := N)) t))) := by
+        rw [mul_stab_quotient_commute_subgroup N t, mul_stab_quotient_commute_subgroup N s]
+        all_goals { aesop }
+    _ ≤ Nat.card N * (card (image (QuotientGroup.mk (s := N)) s ∪
+      image (QuotientGroup.mk (s := N)) t) +
+      card (mulStab (image (QuotientGroup.mk (s := N)) s ∪
+      image (QuotientGroup.mk (s := N)) t))) := Nat.mul_le_mul_left _ this
+    _ ≤ card (s ∪ t) + card (mulStab (s ∪ t)) := by
+      rw [mul_add, ← image_union, subgroup_mul_card_eq_mul_of_mul_stab_subset N (s ∪ t),
+          ← mul_stab_quotient_commute_subgroup N (s ∪ t),
+          subgroup_mul_card_eq_mul_of_mul_stab_subset N (mulStab (s ∪ t))]
+      all_goals
+      { simp only [hNmulstab, mulStab_idem]; norm_cast; exact inter_mulStab_subset_mulStab_union }
+  obtain hst | hst := (subset_union_left s t).eq_or_ssubset
+  · simp [hst.symm]
+  obtain hts | hts := (subset_union_right s t).eq_or_ssubset
+  · simp [hts.symm]
   have : H.card = Hs.card * Ht.card := by
     refine' card_mul_iff.2 fun a ha b hb hab => _
-    sorry
-  suffices Hs.card - H.card ≤ (s \ t).card ∨ Ht.card - H.card ≤ (t \ s).card by sorry
-  set k : α → ℕ := sorry
-  set l : α → ℕ := sorry
+    replace hab : a.2 * b.2⁻¹ = a.1⁻¹ * b.1 := by
+      rw [mul_inv_eq_iff_eq_mul, mul_assoc, ← inv_mul_eq_iff_eq_mul, inv_inv]
+      exact hab
+    have : a.1⁻¹ * b.1 ∈ Hs ∩ Ht := by
+      simp only [mem_inter]
+      constructor
+      · rw [mem_mulStab hs, mul_smul, inv_smul_eq_iff,
+          (mem_mulStab hs).mp (show b.1 ∈ mulStab s by aesop),
+          (mem_mulStab hs).mp (show a.1 ∈ mulStab s by aesop)]
+      · rw [← hab, mem_mulStab ht, mul_comm, mul_smul, inv_smul_eq_iff,
+          (mem_mulStab ht).mp (show b.2 ∈ mulStab t by aesop),
+          (mem_mulStab ht).mp (show a.2 ∈ mulStab t by aesop)]
+    simp only [h1, mem_one] at this
+    ext
+    · rw [← inv_mul_eq_one, this]
+    · rw [← mul_inv_eq_one, hab, this]
+  -- mistake in proof sketch, need to interchange `Hs` and `Ht`
+  suffices h2 : Hs.card - (mulStab (s ∪ t)).card ≤ (s \ t).card ∨
+                Ht.card - (mulStab (s ∪ t)).card ≤ (t \ s).card
+  · simp only [ge_iff_le, min_le_iff]
+    cases' h2 with h2 h2
+    · left
+      sorry
+    · right
+      sorry
+  have Hst : (mulStab (s ∪ t)).Nonempty := Nonempty.mulStab (Nonempty.inr ht)
+  set k : α → ℕ := fun a =>
+    card ((a • H).image (QuotientGroup.mk (s := stabilizer α s)) ∩ s.image QuotientGroup.mk)
+  set l : α → ℕ := fun a =>
+   card ((a • H).image (QuotientGroup.mk (s := stabilizer α t)) ∩ t.image QuotientGroup.mk)
   have hkt : ∀ a, k a ≤ Ht.card := sorry
   have hls : ∀ a, l a ≤ Hs.card := sorry
   have hk : ∀ a, (s \ t ∩ a • H).card = k a * (Hs.card - l a) := by sorry
@@ -75,12 +163,14 @@ lemma le_card_union_add_card_mulStab_union :
       sorry
     · refine' Or.inr ((tsub_eq_zero_of_le <| card_mono _).trans_le <| zero_le _)
       sorry
+  -- the remaining sketch is flawed since `H` is defined to be `Hbar` in Ruzsa's notes and
+  -- `mulStab (s ∪ t) = H` in the notes
   suffices hHst : (Hs.card - 1) * (Ht.card - 1) ≤ (s \ t).card * (t \ s).card
   · by_contra!
     exact
       hHst.not_lt
-        (mul_lt_mul_of_lt_of_lt'' (this.1.trans_le <| tsub_le_tsub_left (one_le_card.2 hH) _) <|
-          this.2.trans_le <| tsub_le_tsub_left (one_le_card.2 hH) _)
+        (mul_lt_mul_of_lt_of_lt'' (this.1.trans_le <| tsub_le_tsub_left (one_le_card.2 Hst) _) <|
+          this.2.trans_le <| tsub_le_tsub_left (one_le_card.2 Hst) _)
   simp (config := {zeta := false}) only
     [not_and_or, not_or, Classical.not_forall, not_ne_iff, not_imp] at hkl
   obtain ⟨a, hka, hka', hla, hla'⟩ | ⟨⟨a, hka, hla⟩, b, hlb, hkb⟩ := hkl
@@ -104,7 +194,8 @@ lemma le_card_union_add_card_mulStab_union :
 
 -- Lemma 3.4 in Ruzsa's notes
 @[to_additive]
-lemma le_card_sup_add_card_mulStab_sup {s : Finset ι} {f : ι → Finset α} (hs : s.Nonempty) :
+lemma le_card_sup_add_card_mulStab_sup {ι : Type*} {s : Finset ι} {f : ι → Finset α}
+    (hs : s.Nonempty) :
     (s.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤
       (s.sup f).card + (s.sup f).mulStab.card := by
   induction' s using Finset.cons_induction with i s hi ih

diff --git a/LeanCamCombi/Kneser/Mathlib.lean b/LeanCamCombi/Kneser/Mathlib.lean
@@ -42,6 +42,25 @@ lemma coe_eq_one : (s : Set α) = 1 ↔ s = ⊥ := (SetLike.ext'_iff.trans (by r
 lemma smul_coe (ha : a ∈ s) : a • (s : Set α) = s := by
   ext; rw [Set.mem_smul_set_iff_inv_smul_mem]; exact Subgroup.mul_mem_cancel_left _ (inv_mem ha)
 
+-- to be simplified
+@[to_additive]
+lemma subgroup_mul_card_eq_mul (s : Subgroup α) (t : Set α) :
+    Nat.card s * Nat.card (t.image (↑) : Set (α ⧸ s)) = Nat.card (t * (s : Set α)) := by
+  rw [← Nat.card_prod, Nat.card_congr]
+  apply Equiv.trans (QuotientGroup.preimageMkEquivSubgroupProdSet _ _).symm
+  rw [QuotientGroup.preimage_image_mk]
+  apply Set.BijOn.equiv id
+  convert Set.bijOn_id _
+  ext x
+  constructor
+  · simp only [Set.mem_iUnion, Set.mem_preimage, Subtype.exists, exists_prop, Set.mem_mul]
+    aesop
+  · simp only [Set.mem_iUnion, Set.mem_preimage, Subtype.exists, exists_prop, forall_exists_index,
+    and_imp]
+    intro y hys hxy
+    rw [← mul_inv_cancel_right x y]
+    apply Set.mul_mem_mul hxy (by simpa)
+
 end Subgroup
 
 namespace Subgroup

diff --git a/LeanCamCombi/Kneser/MulStab.lean b/LeanCamCombi/Kneser/MulStab.lean
@@ -373,4 +373,64 @@ lemma card_mul_card_image_coe (s t : Finset α) :
   -- simp only [h1, h3, Fintype.card_coe] at temp
   -- rw [temp]
 
+@[to_additive]
+lemma subgroup_mul_card_eq_mul_of_mul_stab_subset (s : Subgroup α) (t : Finset α)
+    (hst : (s : Set α) ⊆ t.mulStab) :
+    Nat.card s * card (t.image (↑) : Finset (α ⧸ s)) = card t := by
+  have h : (t : Set α) * s = t := by
+    apply Set.Subset.antisymm (Set.Subset.trans (Set.mul_subset_mul_left hst) _)
+    · intro x
+      rw [Set.mem_mul]
+      aesop
+    · rw [← coe_mul, mul_mulStab]
+  have := s.subgroup_mul_card_eq_mul t
+  rw [h] at this
+  simpa
+
+@[to_additive]
+lemma mul_stab_quotient_commute_subgroup (s : Subgroup α) (t : Finset α)
+    (hst : (s : Set α) ⊆ t.mulStab) :
+    (t.mulStab.image (↑) : Finset (α ⧸ s)) = (t.image (↑) : Finset (α ⧸ s)).mulStab := by
+  obtain rfl | ht := t.eq_empty_or_nonempty
+  · simp
+  have hti : (image (QuotientGroup.mk (s := s)) t).Nonempty := by aesop
+  ext x;
+  simp only [mem_image, Nonempty.image_iff, mem_mulStab hti]
+  constructor
+  · rintro ⟨a, hax⟩
+    rw [← hax.2]
+    ext z
+    simp only [mem_smul_finset, mem_image, smul_eq_mul, exists_exists_and_eq_and]
+    constructor
+    · rintro ⟨b, hbt, hbaz⟩
+      use (b * a)
+      rw [← mul_mulStab t]
+      refine ⟨mul_mem_mul hbt hax.1, ?_⟩
+      rw [← hbaz, QuotientGroup.mk_mul, mul_comm]
+    · rintro ⟨b, hbt, hbz⟩
+      rw [← hbz, ← mul_mulStab t, mul_comm]
+      use (a⁻¹ * b)
+      refine ⟨mul_mem_mul ?_ hbt, by simp⟩
+      rw [← mem_coe, coe_mulStab ht]
+      aesop
+  · intro hx
+    have : s ≤ stabilizer α t := by aesop
+    obtain ⟨y, hyx⟩ := Quotient.exists_rep x
+    refine ⟨y, (mem_mulStab_iff_subset_smul_finset ht).mpr ?_, by simpa⟩
+    intros z hzt
+    replace hx : image QuotientGroup.mk (y • t) = image (QuotientGroup.mk (s := s)) t := by
+      rw [← hx, ← hyx]
+      exact image_smul_comm QuotientGroup.mk y t (congrFun rfl)
+    have hyz : QuotientGroup.mk z ∈ image (QuotientGroup.mk (s := s)) (y • t) := by aesop
+    simp only [QuotientGroup.mk_mul, mem_image] at hyz
+    obtain ⟨a, ha, hayz⟩ := hyz
+    obtain ⟨b, hbt, haby⟩ := mem_smul_finset.mp ha
+    subst a
+    rw [QuotientGroup.eq, smul_eq_mul] at hayz
+    replace : ∃ c ∈ mulStab t, (y • b)⁻¹ * z = c := by aesop
+    obtain ⟨c, hct, hcbyz⟩ := this
+    rw [inv_mul_eq_iff_eq_mul] at hcbyz
+    rw [hcbyz, smul_mul_assoc, mul_comm, ← smul_eq_mul]
+    exact smul_mem_smul_finset ((mem_mulStab' ht).mp hct hbt)
+
 end Finset