From 47bad1cec7395127e01e33b68f6f4fcd80873be4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mantas=20Bak=C5=A1ys?= <39908973+MantasBaksys@users.noreply.github.com> Date: Fri, 22 Dec 2023 15:06:24 +0200 Subject: [PATCH] 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 --- LeanCamCombi/Kneser/KneserRuzsa.lean | 119 +++++++++++++++++++++++---- LeanCamCombi/Kneser/Mathlib.lean | 19 +++++ LeanCamCombi/Kneser/MulStab.lean | 60 ++++++++++++++ 3 files changed, 184 insertions(+), 14 deletions(-) diff --git a/LeanCamCombi/Kneser/KneserRuzsa.lean b/LeanCamCombi/Kneser/KneserRuzsa.lean index 51583b9cfa..4a70af880c 100644 --- 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 index 4facc25a2c..44422db98b 100644 --- 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 index 138bde12ee..31e4d855c8 100644 --- 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