From 4065a8590fd581dec45c210643e30d826254fdce Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sat, 1 Jun 2024 12:33:17 +0000 Subject: [PATCH] Start on the "very small doubling constant" theorem --- LeanAPAP.lean | 2 + LeanAPAP/Extras/FreimanRuzsa.lean | 88 +++++++ LeanAPAP/Extras/FreimanRuzsa/VerySmall.lean | 248 ++++++++++++++++++++ 3 files changed, 338 insertions(+) create mode 100644 LeanAPAP/Extras/FreimanRuzsa.lean create mode 100644 LeanAPAP/Extras/FreimanRuzsa/VerySmall.lean diff --git a/LeanAPAP.lean b/LeanAPAP.lean index 06692dc6c1..852b29f0af 100644 --- a/LeanAPAP.lean +++ b/LeanAPAP.lean @@ -1,4 +1,6 @@ import LeanAPAP.Extras.BSG +import LeanAPAP.Extras.FreimanRuzsa +import LeanAPAP.Extras.FreimanRuzsa.VerySmall import LeanAPAP.FiniteField.Basic import LeanAPAP.Mathlib.Algebra.Group.AddChar import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled diff --git a/LeanAPAP/Extras/FreimanRuzsa.lean b/LeanAPAP/Extras/FreimanRuzsa.lean new file mode 100644 index 0000000000..22ec6e328e --- /dev/null +++ b/LeanAPAP/Extras/FreimanRuzsa.lean @@ -0,0 +1,88 @@ +import Mathlib.Combinatorics.Additive.PluenneckeRuzsa +import Mathlib.Data.Finset.Pointwise +import Mathlib.Data.Real.Basic +import Mathlib.Data.Set.Card +import Mathlib.Tactic.LinearCombination +import Mathlib.Tactic.Positivity.Finset +import Mathlib.Tactic.Rify +import LeanAPAP.Mathlib.Algebra.Group.Subgroup.Basic +import LeanAPAP.Mathlib.Combinatorics.Enumerative.DoubleCounting + +open Finset +open scoped Pointwise + +attribute [norm_cast] Subgroup.coe_set_mk + +variable {G : Type*} [CommGroup G] [DecidableEq G] {K L : ℝ} {A B : Finset G} {a : G} + +/-- If `A` has doubling strictly less than `3 / 2`, then it is contained in a subspace of size at +most `3/2 |A|`. + +This is a very special case of the Freiman-Ruzsa theorem. -/ +theorem IsSmallMul.exists_subgroup_le_three_halves_mul_card (hA : (A * A).card < (3/2 : ℝ) * A.card) + (hA' : A.Nonempty) : + ∃ V : Subgroup G, ∃ a : G, Nat.card V < (3 / 2 : ℝ) * A.card ∧ (A : Set G) ⊆ a • V := by + -- For all `a` and `b`, `a + A` and `b + A` intersect in `> |A| / 2` elements because + -- `|a + A ∪ b + A| ≤ |A + A| < 3/2 |A|` and so + -- `|a + A ∩ b + A| = 2|A| - |a + A ∪ b + A| > |A| / 2`. + have key {a b : G} (ha : a ∈ A) (hb : b ∈ A) : (A.card : ℝ) / 2 < (a • A ∩ b • A).card := + calc + _ = (a • A).card + (b • A).card - (3/2 : ℝ) * A.card := by simp; ring + _ < (a • A).card + (b • A).card - (A * A).card := by gcongr + _ ≤ (a • A).card + (b • A).card - (a • A ∪ b • A).card := by + gcongr; exact union_subset (smul_finset_subset_smul ha) (smul_finset_subset_smul hb) + _ = (a • A ∩ b • A).card := cast_card_inter.symm + -- `A - A` is a subgroup since clearly it contains `0` and is closed under negation, and further + -- if `a, b, c, d ∈ A` then `|A ∩ a - b + A| + |A ∩ d - c + A| > |A|` so `a - b + A` and + -- `d - c + A` intersect, meaning that `(a - b) + (c - d) ∈ A - A`. + use + { carrier := A / A, + one_mem' := by simp [hA'.ne_empty] + mul_mem' := by + rintro _ _ ⟨a, ha, b, hb, rfl⟩ ⟨c, hc, d, hd, rfl⟩ + obtain ⟨_, ⟨e, he, hef⟩, ⟨f, hf, rfl⟩⟩ : ((a / b) • A ∩ (d / c) • A : Set G).Nonempty := by + norm_cast + refine Nonempty.mono (s := ((a / b) • A ∩ A) ∩ ((d / c) • A ∩ A)) + (by gcongr <;> apply inter_subset_left) $ inter_nonempty_of_card_lt_card_add_card + (inter_subset_right ..) (inter_subset_right ..) ?_ + rw [← card_smul_finset b (_ ∩ _), ← card_smul_finset c (_ ∩ _), smul_finset_inter, + smul_finset_inter, smul_smul, smul_smul, mul_div_cancel, mul_div_cancel] + rify + linarith [key ha hb, key hd hc] + refine ⟨_, hf, _, he, ?_⟩ + dsimp at hef ⊢ + rwa [mul_comm _ f, ← div_eq_div_iff_mul_eq_mul, div_div_eq_mul_div, eq_comm, mul_div_assoc] + at hef + inv_mem' := by rintro _ ⟨a, ha, b, hb, rfl⟩; exact ⟨b, hb, a, ha, by simp⟩ } + have : (A / A).card / (2 : ℝ) < A.card := by + refine lt_of_mul_lt_mul_of_nonneg_left ?_ A.card.cast_nonneg + calc + _ = (A / A).card • (A.card / 2 : ℝ) := by ring + _ < (A ×ˢ A).card • 1 := + card_nsmul_lt_card_nsmul_of_lt_of_le (fun x (a, b) ↦ x = a / b) (hA'.div hA') ?_ ?_ + _ = A.card * A.card := by simp [sq] + · simp only [bipartiteAbove, mem_div] + rintro _ ⟨a, ha, b, hb, rfl⟩ + refine (key ha hb).trans_le ?_ + norm_cast + refine card_le_card_of_surjOn (fun (c, d) ↦ c * b) ?_ + · simp only [Set.SurjOn, coe_inter, coe_smul_finset, coe_filter, mem_product, Set.subset_def, + Set.mem_inter_iff, Set.mem_image, Set.mem_setOf_eq, Prod.exists, and_imp, and_assoc] + rintro _ ⟨c, hc, hcd⟩ ⟨d, hd, rfl⟩ + dsimp at hcd ⊢ + exact ⟨d, c, hd, hc, by rw [div_eq_div_iff_mul_eq_mul, hcd, mul_comm], mul_comm ..⟩ + · simp (config := { contextual := true }) [bipartiteBelow, card_le_one] + simp only [Subgroup.mem_mk, Nat.card_eq_fintype_card, ← coe_div, Fintype.card_coe, mem_coe] + obtain ⟨a, ha⟩ := hA' + refine ⟨a, ?_, ?_⟩ + · calc + _ ≤ ((a⁻¹ • A * a⁻¹ • A).card : ℝ) := ?_ + _ = (A * A).card := by simp [smul_mul_assoc, mul_smul_comm] + _ < 3 / 2 * A.card := hA + gcongr + rintro v hv + sorry + · norm_cast + norm_cast -- Strange. Why is `norm_cast` not idempotent? + rw [← inv_mul_eq_div, subset_smul_finset_iff] + exact smul_finset_subset_smul (inv_mem_inv ha) diff --git a/LeanAPAP/Extras/FreimanRuzsa/VerySmall.lean b/LeanAPAP/Extras/FreimanRuzsa/VerySmall.lean new file mode 100644 index 0000000000..5d9d8cd622 --- /dev/null +++ b/LeanAPAP/Extras/FreimanRuzsa/VerySmall.lean @@ -0,0 +1,248 @@ +import Mathlib + +open scoped Pointwise + +open Finset MulOpposite + +variable {G : Type*} [DecidableEq G] [Group G] {A B : Finset G} + +-- Throughout this file I use {x} * A rather than x • A largely because x • A is surprisingly +-- tricky to work with. +-- TODO: (maybe Yaël, who's thought about this a lot already?) make the API for x • A (in both Set +-- and Finset) better. + +lemma singleton_mul_eq_smul {a : G} : {a} * A = a • A := singleton_mul _ +lemma smul_finset_subset_mul {a : G} : a ∈ A → a • B ⊆ A * B := image_subset_image₂_right + +-- This came up a few times, it's useful to get size bounds on xA ∩ yA +lemma big_intersection {x y : G} (hx : x ∈ A) (hy : y ∈ A) : + 2 * A.card ≤ ((x • A) ∩ (y • A)).card + (A * A).card := by + have : ((x • A) ∪ (y • A)).card ≤ (A * A).card := by + refine card_le_card ?_ + rw [union_subset_iff] + exact ⟨smul_finset_subset_mul hx, smul_finset_subset_mul hy⟩ + refine (add_le_add_left this _).trans_eq' ?_ + rw [card_inter_add_card_union] + simp only [card_smul_finset, two_mul] + +lemma mul_comm_of_doubling_aux (h : (A * A).card < 2 * A.card) : A⁻¹ * A ⊆ A * A⁻¹ := by + intro z + simp only [mem_mul, forall_exists_index, exists_and_left, and_imp, mem_inv, + exists_exists_and_eq_and] + rintro x hx y hy rfl + have ⟨t, ht⟩ : ((x • A) ∩ (y • A)).Nonempty := by + rw [←card_pos] + linarith [big_intersection hx hy] + simp only [mem_inter, mem_smul_finset, smul_eq_mul] at ht + obtain ⟨⟨z, hz, hzxwy⟩, w, hw, rfl⟩ := ht + refine ⟨z, hz, w, hw, ?_⟩ + rw [mul_inv_eq_iff_eq_mul, mul_assoc, ←hzxwy, inv_mul_cancel_left] + +-- TODO: is there a way to get wlog to make `mul_comm_of_doubling_aux` a goal? +-- ie wlog in the target rather than hypothesis +-- (BM: third time seeing this pattern) +-- I'm thinking something like wlog_suffices, where I could write +-- wlog_suffices : A⁻¹ * A ⊆ A * A⁻¹ +-- which reverts *everything* (just like wlog does) and makes the side goal A⁻¹ * A = A * A⁻¹ +-- under the assumption A⁻¹ * A ⊆ A * A⁻¹ +-- and changes the main goal to A⁻¹ * A ⊆ A * A⁻¹ +lemma mul_comm_of_doubling (h : (A * A).card < 2 * A.card) : + A * A⁻¹ = A⁻¹ * A := by + refine Finset.Subset.antisymm ?_ (mul_comm_of_doubling_aux h) + have : A⁻¹⁻¹ * A⁻¹ ⊆ A⁻¹ * A⁻¹⁻¹ := by + refine mul_comm_of_doubling_aux ?_ + simpa only [card_inv, ←mul_inv_rev] + rwa [inv_inv] at this + +lemma coe_mul_comm_of_doubling (h : (A * A).card < 2 * A.card) : + (A * A⁻¹ : Set G) = A⁻¹ * A := by + rw [←Finset.coe_mul, mul_comm_of_doubling h, Finset.coe_mul] + +lemma weaken_doubling (h : (A * A).card < (3 / 2 : ℚ) * A.card) : + (A * A).card < 2 * A.card := by + rw [←Nat.cast_lt (α := ℚ), Nat.cast_mul, Nat.cast_two] + linarith only [h] + +lemma nonempty_of_doubling (h : (A * A).card < (3 / 2 : ℚ) * A.card) : + A.Nonempty := by + rw [nonempty_iff_ne_empty] + rintro rfl + simp at h + +example {a b c : G} : (a * b) * (b⁻¹ * c) = a * c := by + simp [mul_assoc] + -- MulAction.injective a + +/-- +TODO: better docstring +The subgroup of G that we will show covers a translate of A while not being a lot bigger than +it. While this is clearly a symmetric set that contains 1, showing it's closed under multiplication +uses the doubling hypothesis heavily. +I'm pretty sure 3/2 is sharp for A⁻¹A to be a subgroup? +-/ +@[simps] +def symmetricSubgroup (A : Finset G) (h : (A * A).card < (3 / 2 : ℚ) * A.card) : Subgroup G where + carrier := A⁻¹ * A + one_mem' := by + have ⟨x, hx⟩ : A.Nonempty := nonempty_of_doubling h + exact ⟨x⁻¹, inv_mem_inv hx, x, by simp [hx]⟩ + inv_mem' := by + intro x + simp only [Set.mem_mul, Set.mem_inv, coe_inv, forall_exists_index, exists_and_left, mem_coe, + and_imp] + rintro a ha b hb rfl + exact ⟨b⁻¹, by simpa using hb, a⁻¹, ha, by simp⟩ + mul_mem' := by + have h₁ : ∀ x ∈ A, ∀ y ∈ A, (1 / 2 : ℚ) * A.card < (x • A ∩ y • A).card := by + intro x hx y hy + have := big_intersection hx hy + rw [←Nat.cast_le (α := ℚ), Nat.cast_mul, Nat.cast_add, Nat.cast_two] at this + linarith + intro a c ha hc + simp only [Set.mem_mul, Set.mem_inv, coe_inv, mem_coe, exists_and_left] at ha hc + obtain ⟨a, ha, b, hb, rfl⟩ := ha + obtain ⟨c, hc, d, hd, rfl⟩ := hc + have h₂ : (1 / 2 : ℚ) * A.card < (A ∩ (a * b)⁻¹ • A).card := by + refine (h₁ b hb _ ha).trans_le ?_ + rw [←card_smul_finset b⁻¹] + simp [smul_smul, smul_finset_inter] + have h₃ : (1 / 2 : ℚ) * A.card < (A ∩ (c * d) • A).card := by + refine (h₁ _ hc d hd).trans_le ?_ + rw [←card_smul_finset c] + simp [smul_smul, smul_finset_inter] + have ⟨t, ht⟩ : ((A ∩ (c * d) • A) ∩ (A ∩ (a * b)⁻¹ • A)).Nonempty := by + rw [←Finset.card_pos, ←Nat.cast_pos (α := ℚ)] + have := card_inter_add_card_union (A ∩ (c * d) • A) (A ∩ (a * b)⁻¹ • A) + rw [←Nat.cast_inj (R := ℚ), Nat.cast_add, Nat.cast_add] at this + have : (((A ∩ (c * d) • A) ∪ (A ∩ (a * b)⁻¹ • A)).card : ℚ) ≤ A.card := by + rw [Nat.cast_le, ← inter_union_distrib_left] + exact card_le_card inter_subset_left + linarith + simp only [inter_inter_inter_comm, inter_self, mem_inter, ←inv_smul_mem_iff, inv_inv, + smul_eq_mul, mul_assoc, mul_inv_rev] at ht + rw [←coe_mul_comm_of_doubling (weaken_doubling h)] + exact ⟨a * b * t, by simp [ht, mul_assoc], ((c * d)⁻¹ * t)⁻¹, by simp [ht, mul_assoc]⟩ + +lemma two_two_two (h : (A * A).card < (3 / 2 : ℚ) * A.card) : + ∃ H : Subgroup G, (H : Set G) = A⁻¹ * A := + ⟨symmetricSubgroup _ h, rfl⟩ + +lemma weak_symmetricSubgroup_bound (h : (A * A).card < (3 / 2 : ℚ) * A.card) : + (A⁻¹ * A).card < 2 * A.card := by + have h₀ : A.Nonempty := nonempty_of_doubling h + have h₁ : ∀ x ∈ A, ∀ y ∈ A, (1 / 2 : ℚ) * A.card < ((x • A) ∩ (y • A)).card := by + intro x hx y hy + have := big_intersection hx hy + rw [←Nat.cast_le (α := ℚ), Nat.cast_mul, Nat.cast_add, Nat.cast_two] at this + linarith + have h₂ : ∀ a ∈ A⁻¹ * A, + (1 / 2 : ℚ) * A.card < ((A ×ˢ A).filter (fun ⟨x, y⟩ => x * y⁻¹ = a)).card := by + simp only [mem_mul, mem_product, Prod.forall, and_imp, mem_inv, exists_exists_and_eq_and, + forall_exists_index] + rintro _ a ha b hb rfl + refine (h₁ a ha b hb).trans_le ?_ + rw [Nat.cast_le] + refine card_le_card_of_injOn (fun t => (a⁻¹ * t, b⁻¹ * t)) ?_ (by simp [Set.InjOn]) + simp only [mem_inter, mem_product, and_imp, Prod.forall, mem_filter, mul_inv_rev, inv_inv, + exists_and_left, exists_eq_left, forall_exists_index, smul_eq_mul, + forall_apply_eq_imp_iff₂, inv_mul_cancel_left, inv_mul_cancel_right, mem_smul_finset] + rintro c hc d hd h + rw [mul_assoc, mul_inv_cancel_left, ← h, inv_mul_cancel_left] + simp [hd, hc] + have h₃ : ∀ x ∈ A ×ˢ A, (fun ⟨x, y⟩ => x * y⁻¹) x ∈ A⁻¹ * A := by + rw [←mul_comm_of_doubling (weaken_doubling h)] + simp only [mem_product, Prod.forall, mem_mul, and_imp, mem_inv] + intro a b ha hb + exact ⟨a, ha, b⁻¹, by simp [hb], rfl⟩ + have : ((1 / 2 : ℚ) * A.card) * (A⁻¹ * A).card < (A.card : ℚ) ^ 2 := by + rw [←Nat.cast_pow, sq, ←card_product, card_eq_sum_card_fiberwise h₃, Nat.cast_sum] + refine (Finset.sum_lt_sum_of_nonempty (by simp [h₀]) h₂).trans_eq' ?_ + simp only [sum_const, nsmul_eq_mul, mul_comm] + have : (0 : ℚ) < A.card := by simpa [card_pos] + rw [←Nat.cast_lt (α := ℚ), Nat.cast_mul, Nat.cast_two] + -- passing between ℕ- and ℚ-inequalities is annoying, here and above + nlinarith + +lemma A_subset_aH (a : G) (ha : a ∈ A) : A ⊆ a • (A⁻¹ * A) := by + rw [←smul_mul_assoc] + exact subset_mul_right _ (by simp [←inv_smul_mem_iff, inv_mem_inv ha]) + +lemma subgroup_strong_bound_left (h : (A * A).card < (3 / 2 : ℚ) * A.card) (a : G) (ha : a ∈ A) : + A * A ⊆ a • op a • (A⁻¹ * A) := by + have h₁ : (A⁻¹ * A) * (A⁻¹ * A) = A⁻¹ * A := by + rw [←Finset.coe_inj, coe_mul, coe_mul, ←symmetricSubgroup_coe _ h, coe_mul_coe] + have h₂ : a • op a • (A⁻¹ * A) = (a • (A⁻¹ * A)) * (op a • (A⁻¹ * A)) := by + rw [mul_smul_comm, smul_mul_assoc, h₁, smul_comm] + rw [h₂] + refine mul_subset_mul (A_subset_aH a ha) ?_ + rw [←mul_comm_of_doubling (weaken_doubling h), ←mul_smul_comm] + exact subset_mul_left _ (by simp [←inv_smul_mem_iff, inv_mem_inv ha]) + +lemma subgroup_strong_bound_right (h : (A * A).card < (3 / 2 : ℚ) * A.card) (a : G) (ha : a ∈ A) : + a • op a • (A⁻¹ * A) ⊆ A * A := by + intro z hz + obtain ⟨H, hH⟩ := two_two_two h + simp only [mem_smul_finset, smul_eq_mul_unop, unop_op, smul_eq_mul, mem_mul, mem_inv, + exists_exists_and_eq_and, exists_and_left] at hz + obtain ⟨d, ⟨b, hb, c, hc, rfl⟩, hz⟩ := hz + let l : Finset G := A ∩ ((z * a⁻¹) • (A⁻¹ * A)) + -- ^ set of x ∈ A st ∃ y ∈ H a with x y = z + let r : Finset G := (a • (A⁻¹ * A)) ∩ (z • A⁻¹) + -- ^ set of x ∈ a H st ∃ y ∈ A with x y = z + have : (A⁻¹ * A) * (A⁻¹ * A) = A⁻¹ * A := by + rw [←Finset.coe_inj, coe_mul, coe_mul, ←hH, coe_mul_coe] + have hl : l = A := by + rw [inter_eq_left, ←this, subset_smul_finset_iff] + simp only [←hz, mul_inv_rev, inv_inv, ←mul_assoc] + refine smul_finset_subset_mul ?_ + simp [mul_mem_mul, mem_inv, ha, hb, hc] + have hr : r = z • A⁻¹ := by + rw [inter_eq_right, ←this, mul_assoc _ A, ←mul_comm_of_doubling (weaken_doubling h), + subset_smul_finset_iff] + simp only [←mul_assoc, smul_smul] + refine smul_finset_subset_mul ?_ + simp [←hz, mul_mem_mul, ha, hb, hc, mem_inv] + have lr : l ∪ r ⊆ a • (A⁻¹ * A) := by + rw [union_subset_iff, hl] + exact ⟨A_subset_aH a ha, inter_subset_left⟩ + have : l.card = A.card := by rw [hl] + have : r.card = A.card := by rw [hr, card_smul_finset, card_inv] + have : (l ∪ r).card < 2 * A.card := by + refine (card_le_card lr).trans_lt ?_ + rw [card_smul_finset] + exact weak_symmetricSubgroup_bound h + have ⟨t, ht⟩ : (l ∩ r).Nonempty := by + rw [←card_pos] + linarith [card_inter_add_card_union l r] + simp only [hl, hr, mem_inter, ←inv_smul_mem_iff, smul_eq_mul, Finset.mem_inv', mul_inv_rev, + inv_inv] at ht + rw [mem_mul] + exact ⟨t, ht.1, t⁻¹ * z, ht.2, by simp⟩ + +lemma subgroup_strong_bound_equality (h : (A * A).card < (3 / 2 : ℚ) * A.card) + (a : G) (ha : a ∈ A) : + a • op a • (A⁻¹ * A) = A * A := + (subgroup_strong_bound_right h a ha).antisymm (subgroup_strong_bound_left h a ha) + +lemma subgroup_strong_bound (h : (A * A).card < (3 / 2 : ℚ) * A.card) : + (A⁻¹ * A).card = (A * A).card := by + obtain ⟨a, ha⟩ := nonempty_of_doubling h + rw [←subgroup_strong_bound_equality h a ha, card_smul_finset, card_smul_finset] + +theorem very_small_doubling (A : Finset G) (h : (A * A).card < (3 / 2 : ℚ) * A.card) : + ∃ (H : Subgroup G), ∃ a ∈ A, + (H : Set G).ncard < (3 / 2 : ℚ) * A.card ∧ + (A : Set G) ⊆ a • (H : Set G) := by + have ⟨a, ha⟩ := nonempty_of_doubling h + refine ⟨symmetricSubgroup _ h, a, ha, ?_, ?_⟩ + · rwa [symmetricSubgroup_coe, ←coe_mul, Set.ncard_coe_Finset, subgroup_strong_bound h] + · rw [symmetricSubgroup_coe] + exact_mod_cast A_subset_aH a ha + +-- a A⁻¹ A a⁻¹ ⊆ A⁻¹ A ? + +-- lemma very_small_doubling_normalizer (h : (A * A).card < (3 / 2 : ℚ) * A.card) +-- (a : G) (ha : a ∈ A) : +-- {a} * (A⁻¹ * A) = (A⁻¹ * A) * {a} := by +-- suffices : {a} * (A⁻¹ * A) * {a⁻¹} = A⁻¹ * A +-- ·