From 6a298624d57f24e948c7d6669cd9c27d7bf74cfa Mon Sep 17 00:00:00 2001 From: Gabriel Dahia Date: Sun, 8 Nov 2026 18:33:34 +0100 Subject: [PATCH 1/2] Import Ruzsa's sum of sets in several dimensions MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Import the formalization of Ruzsa, "Sum of sets in several dimensions" (Combinatorica 14 (1994), doi:10.1007/BF01302969), from gdahia/SumOfSetsInSeveralDimensions at bd2694b: the lower bound |A + B| ≥ |A| + Σ min(d, |A| - t) for sumsets of affine dimension d in R^D, its sharpness (Theorem 2), the asymmetric Freiman lemma, and bounds on the Freiman dimension of sets of small doubling. The library moves under LeanPool.SumOfSetsInSeveralDimensions with its imports rewritten, and the unused [DecidableEq G] arguments of freimanModelDim, freimanDim and three lemmas about them are dropped for the unused-arguments linter. The Palomar Challenge and Solution modules are left out, since Solution only restates the library theorems. Co-Authored-By: Claude Opus 5.5 --- LeanPool/SumOfSetsInSeveralDimensions.lean | 37 ++ .../AffineDim.lean | 118 ++++++ .../AffineDimSumset.lean | 87 +++++ .../ClosedForm.lean | 113 ++++++ .../Construction.lean | 237 +++++++++++ .../FreimanDimension.lean | 69 ++++ .../FreimanDimensionSumsetBounds.lean | 326 ++++++++++++++++ .../GeometricDeletion.lean | 368 ++++++++++++++++++ .../SumOfSetsInSeveralDimensions/Imports.lean | 21 + .../LowerBound.lean | 113 ++++++ .../LowerBoundFunction.lean | 111 ++++++ .../LowerBoundValues.lean | 98 +++++ .../MinCardAdd.lean | 111 ++++++ .../Normalize.lean | 97 +++++ .../sum-of-sets-in-several-dimensions.yaml | 68 ++++ 15 files changed, 1974 insertions(+) create mode 100644 LeanPool/SumOfSetsInSeveralDimensions.lean create mode 100644 LeanPool/SumOfSetsInSeveralDimensions/AffineDim.lean create mode 100644 LeanPool/SumOfSetsInSeveralDimensions/AffineDimSumset.lean create mode 100644 LeanPool/SumOfSetsInSeveralDimensions/ClosedForm.lean create mode 100644 LeanPool/SumOfSetsInSeveralDimensions/Construction.lean create mode 100644 LeanPool/SumOfSetsInSeveralDimensions/FreimanDimension.lean create mode 100644 LeanPool/SumOfSetsInSeveralDimensions/FreimanDimensionSumsetBounds.lean create mode 100644 LeanPool/SumOfSetsInSeveralDimensions/GeometricDeletion.lean create mode 100644 LeanPool/SumOfSetsInSeveralDimensions/Imports.lean create mode 100644 LeanPool/SumOfSetsInSeveralDimensions/LowerBound.lean create mode 100644 LeanPool/SumOfSetsInSeveralDimensions/LowerBoundFunction.lean create mode 100644 LeanPool/SumOfSetsInSeveralDimensions/LowerBoundValues.lean create mode 100644 LeanPool/SumOfSetsInSeveralDimensions/MinCardAdd.lean create mode 100644 LeanPool/SumOfSetsInSeveralDimensions/Normalize.lean create mode 100644 LeanPool/projects/sum-of-sets-in-several-dimensions.yaml diff --git a/LeanPool/SumOfSetsInSeveralDimensions.lean b/LeanPool/SumOfSetsInSeveralDimensions.lean new file mode 100644 index 0000000000..f232a9aa4e --- /dev/null +++ b/LeanPool/SumOfSetsInSeveralDimensions.lean @@ -0,0 +1,37 @@ +/- +Copyright (c) 2026 Gabriel Dahia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Dahia +-/ +module + +public import LeanPool.SumOfSetsInSeveralDimensions.ClosedForm +public import LeanPool.SumOfSetsInSeveralDimensions.FreimanDimensionSumsetBounds +public import LeanPool.SumOfSetsInSeveralDimensions.LowerBound +public import LeanPool.SumOfSetsInSeveralDimensions.MinCardAdd + +/-! +# Sum of sets in several dimensions + +Source: doi:10.1007/BF01302969, url:https://github.com/gdahia/SumOfSetsInSeveralDimensions/tree/bd2694b89fbe18ee5c4365a6330eba36d9f7ed8e +Authors: Gabriel Dahia +Status: verified +Main declarations: + `SumOfSetsInSeveralDimensions.card_add_sum_min_le_card_add_of_finrank_span_sub_eq`, + `SumOfSetsInSeveralDimensions.card_add_mul_card_le_card_add_add_of_le_finrank_span_sub`, + `SumOfSetsInSeveralDimensions.sInf_card_add_eq_add_sum_min`, + `SumOfSetsInSeveralDimensions.freimanDim_le_two_mul_sub_one_of_card_add_le` +Tags: additive-combinatorics, sumsets, freiman-dimension, discrete-geometry +MSC: 11P70, 11B13, 11B75 +-/ + +/-! +## Upstream attribution + +Adapted for Lean Pool from upstream commit `bd2694b89fbe18ee5c4365a6330eba36d9f7ed8e` by +moving the library under `LeanPool.SumOfSetsInSeveralDimensions` and by dropping the unused +`[DecidableEq G]` arguments of `freimanModelDim`, `freimanDim` and three lemmas about them, which +Mathlib's unused-arguments linter rejects. The upstream Palomar +`Challenge` and `Solution` modules are omitted: `Solution` only restates library theorems under +primed names. +-/ diff --git a/LeanPool/SumOfSetsInSeveralDimensions/AffineDim.lean b/LeanPool/SumOfSetsInSeveralDimensions/AffineDim.lean new file mode 100644 index 0000000000..cc1e1415b9 --- /dev/null +++ b/LeanPool/SumOfSetsInSeveralDimensions/AffineDim.lean @@ -0,0 +1,118 @@ +/- +Copyright (c) 2026 Gabriel Dahia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Dahia +-/ +module + +public import Mathlib.Algebra.Group.Pointwise.Finset.Scalar +public import Mathlib.Basic.Real.Basic +public import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic +public import Mathlib.LinearAlgebra.Dimension.Finrank +import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional + +/-! +# Affine dimension of a finite set + +The affine dimension of a finite set `S ⊆ ℝ^D` is the dimension of the direction of its affine +span. The direction of the affine span of `S` is the vector span of `S`, the subspace spanned by +the differences of the points of `S`. + +## Main definitions + +* `Finset.affineDim S`: the affine dimension of `S`. + +## Main statements + +* `Finset.affineDim_eq_finrank_vectorSpan`: `S.affineDim` is the dimension of `vectorSpan ℝ S`. +* `Finset.affineDim_eq_finrank_span_sub`: `S.affineDim` is the dimension of the span of `S - S`. +* `Finset.affineDim_mono`: the affine dimension is monotone. +* `Finset.affineDim_vadd_finset`, `Finset.affineDim_image_add_left`, + `Finset.affineDim_image_add_right`, `Finset.affineDim_image_sub`: it is invariant under + translation. +* `Finset.affineDim_add_one_le_card`: a nonempty set of affine dimension `d` has at least `d + 1` + points. +-/ + +@[expose] public section + +namespace Finset + +open scoped Pointwise + +variable {D : ℕ} + +/-- The affine dimension of a finite set `S ⊆ ℝ^D`: the dimension of the direction of the affine +span of `S`. -/ +noncomputable def affineDim (S : Finset (Fin D → ℝ)) : ℕ := + Module.finrank ℝ (affineSpan ℝ (S : Set (Fin D → ℝ))).direction + +/-- The affine dimension of `S` is the dimension of the vector span of `S`. -/ +lemma affineDim_eq_finrank_vectorSpan (S : Finset (Fin D → ℝ)) : + S.affineDim = Module.finrank ℝ (vectorSpan ℝ (S : Set (Fin D → ℝ))) := by + rw [affineDim, direction_affineSpan] + +/-- The affine dimension of `S` is the dimension of the span of `S - S`. -/ +lemma affineDim_eq_finrank_span_sub (S : Finset (Fin D → ℝ)) : + S.affineDim = Module.finrank ℝ (Submodule.span ℝ (↑S - ↑S : Set (Fin D → ℝ))) := by + rw [affineDim_eq_finrank_vectorSpan, vectorSpan_def] + rfl + +/-- Affine dimension is monotone under inclusion of finite sets. -/ +lemma affineDim_mono {S T : Finset (Fin D → ℝ)} + (hST : S ⊆ T) : S.affineDim ≤ T.affineDim := by + unfold affineDim + apply Submodule.finrank_mono + apply AffineSubspace.direction_le + apply affineSpan_mono + simpa using hST + +/-- The affine dimension of a subset of `ℝ^D` is at most `D`. -/ +lemma affineDim_le (S : Finset (Fin D → ℝ)) : S.affineDim ≤ D := + (Submodule.finrank_le _).trans_eq (Module.finrank_fin_fun ℝ) + +@[simp] +lemma affineDim_empty : (∅ : Finset (Fin D → ℝ)).affineDim = 0 := by + simp [affineDim_eq_finrank_vectorSpan] + +@[simp] +lemma affineDim_singleton (x : Fin D → ℝ) : ({x} : Finset (Fin D → ℝ)).affineDim = 0 := by + simp [affineDim_eq_finrank_vectorSpan] + +/-- The affine dimension is invariant under translation. -/ +@[simp] +lemma affineDim_vadd_finset (c : Fin D → ℝ) (S : Finset (Fin D → ℝ)) : + (c +ᵥ S).affineDim = S.affineDim := by + rw [affineDim_eq_finrank_vectorSpan, coe_vadd_finset, vectorSpan_vadd, + affineDim_eq_finrank_vectorSpan] + +/-- The affine dimension of `c + S` is that of `S`. -/ +lemma affineDim_image_add_left (c : Fin D → ℝ) (S : Finset (Fin D → ℝ)) : + (S.image (c + ·)).affineDim = S.affineDim := + affineDim_vadd_finset c S + +/-- The affine dimension of `S + c` is that of `S`. -/ +lemma affineDim_image_add_right (c : Fin D → ℝ) (S : Finset (Fin D → ℝ)) : + (S.image (· + c)).affineDim = S.affineDim := by + simp only [add_comm _ c, affineDim_image_add_left] + +/-- The affine dimension of `S - c` is that of `S`. -/ +lemma affineDim_image_sub (S : Finset (Fin D → ℝ)) (c : Fin D → ℝ) : + (S.image fun x ↦ x - c).affineDim = S.affineDim := by + simp only [sub_eq_add_neg, affineDim_image_add_right] + +/-- A nonempty finite set of affine dimension `d` contains at least `d + 1` points. -/ +lemma affineDim_add_one_le_card {S : Finset (Fin D → ℝ)} (hS : S.Nonempty) : + S.affineDim + 1 ≤ #S := by + have : Nonempty (S : Set (Fin D → ℝ)) := hS.to_set.to_subtype + have h := finrank_vectorSpan_range_add_one_le ℝ ((↑) : ↥(S : Set (Fin D → ℝ)) → Fin D → ℝ) + rw [Subtype.range_coe, ← affineDim_eq_finrank_vectorSpan] at h + simpa using h + +/-- The affine dimension of a finite set is at most its number of points. -/ +lemma affineDim_le_card (S : Finset (Fin D → ℝ)) : S.affineDim ≤ #S := by + obtain rfl | hS := S.eq_empty_or_nonempty + · simp + · grind [affineDim_add_one_le_card hS] + +end Finset diff --git a/LeanPool/SumOfSetsInSeveralDimensions/AffineDimSumset.lean b/LeanPool/SumOfSetsInSeveralDimensions/AffineDimSumset.lean new file mode 100644 index 0000000000..cc96481d6c --- /dev/null +++ b/LeanPool/SumOfSetsInSeveralDimensions/AffineDimSumset.lean @@ -0,0 +1,87 @@ +/- +Copyright (c) 2026 Gabriel Dahia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Dahia +-/ +module + +public import LeanPool.SumOfSetsInSeveralDimensions.AffineDim +public import Mathlib.Algebra.Group.Pointwise.Finset.Basic +import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional +import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas + +/-! +# Affine dimension of a sumset + +The affine dimension of `A + B` is at least the affine dimensions of `A` and of `B` when both +sets are nonempty, and at least the affine dimension of `A ∪ B` minus one. + +## Main statements + +* `Finset.affineDim_le_affineDim_add_right`, `Finset.affineDim_le_affineDim_add_left`: the + affine dimensions of `A` and `B` are at most that of `A + B`. +* `Finset.affineDim_add_eq_of_left_eq`: if `A ⊆ ℝ^D` has affine dimension `D`, so has `A + B`. +* `Finset.affineDim_union_le_sum_add_one`: the affine dimension of `A ∪ B` is at most that + of `A + B` plus one. +-/ + +public section + +namespace Finset + +open scoped Pointwise + +variable {D : ℕ} + +/-- The affine dimension of `A` is at most that of `A + B` when `B` is nonempty. -/ +lemma affineDim_le_affineDim_add_right (A : Finset (Fin D → ℝ)) + {B : Finset (Fin D → ℝ)} (hB : B.Nonempty) : A.affineDim ≤ (A + B).affineDim := by + obtain ⟨b, hb⟩ := hB + rw [← affineDim_image_add_right b A] + apply affineDim_mono + rw [image_subset_iff] + intro a ha + exact add_mem_add ha hb + +/-- The affine dimension of `B` is at most that of `A + B` when `A` is nonempty. -/ +lemma affineDim_le_affineDim_add_left {A : Finset (Fin D → ℝ)} (hA : A.Nonempty) + (B : Finset (Fin D → ℝ)) : B.affineDim ≤ (A + B).affineDim := by + rw [add_comm] + exact affineDim_le_affineDim_add_right B hA + +/-- If `A ⊆ ℝ^D` has affine dimension `D` and `B` is nonempty, then `A + B` has affine +dimension `D`. -/ +lemma affineDim_add_eq_of_left_eq {A B : Finset (Fin D → ℝ)} (hB : B.Nonempty) + (hA : A.affineDim = D) : (A + B).affineDim = D := + le_antisymm (affineDim_le _) + (hA.symm.trans_le (affineDim_le_affineDim_add_right A hB)) + +private lemma vectorSpan_union_le {A B : Finset (Fin D → ℝ)} {a b : Fin D → ℝ} (ha : a ∈ A) + (hb : b ∈ B) : + vectorSpan ℝ (↑(A ∪ B) : Set (Fin D → ℝ)) ≤ + vectorSpan ℝ (↑(A + B) : Set (Fin D → ℝ)) ⊔ Submodule.span ℝ {b - a} := by + rw [vectorSpan_eq_span_vsub_set_right ℝ (p := a) (by simp [ha]), Submodule.span_le] + rintro v ⟨x, hx, rfl⟩ + simp only [vsub_eq_sub, SetLike.mem_coe] + obtain hx | hx := mem_union.1 hx + · apply le_sup_left (b := Submodule.span ℝ {b - a}) + simpa using vsub_mem_vectorSpan ℝ (mem_coe.2 (add_mem_add hx hb)) + (mem_coe.2 (add_mem_add ha hb)) + · rw [← sub_add_sub_cancel x b a] + apply Submodule.add_mem_sup _ (Submodule.mem_span_singleton_self _) + simpa using vsub_mem_vectorSpan ℝ (mem_coe.2 (add_mem_add ha hx)) + (mem_coe.2 (add_mem_add ha hb)) + +/-- The affine span of `A ∪ B` has dimension at most one more than the affine span of `A + B`. -/ +lemma affineDim_union_le_sum_add_one {A B : Finset (Fin D → ℝ)} + (hA : A.Nonempty) (hB : B.Nonempty) : + (A ∪ B).affineDim ≤ (A + B).affineDim + 1 := by + obtain ⟨a, ha⟩ := hA + obtain ⟨b, hb⟩ := hB + rw [affineDim_eq_finrank_vectorSpan, affineDim_eq_finrank_vectorSpan] + apply (Submodule.finrank_mono (vectorSpan_union_le ha hb)).trans + apply (Submodule.finrank_add_le_finrank_add_finrank _ _).trans + gcongr + simpa using finrank_span_le_card ({b - a} : Set (Fin D → ℝ)) + +end Finset diff --git a/LeanPool/SumOfSetsInSeveralDimensions/ClosedForm.lean b/LeanPool/SumOfSetsInSeveralDimensions/ClosedForm.lean new file mode 100644 index 0000000000..d8bb179267 --- /dev/null +++ b/LeanPool/SumOfSetsInSeveralDimensions/ClosedForm.lean @@ -0,0 +1,113 @@ +/- +Copyright (c) 2026 Gabriel Dahia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Dahia +-/ +module + +public import LeanPool.SumOfSetsInSeveralDimensions.AffineDim +public import Mathlib.Algebra.BigOperators.Group.Finset.Basic +public import Mathlib.Algebra.Group.Pointwise.Finset.Basic +public import Mathlib.Order.Interval.Finset.Nat +import LeanPool.SumOfSetsInSeveralDimensions.LowerBound +import Mathlib.Algebra.BigOperators.Intervals +import Mathlib.Algebra.Order.BigOperators.Group.Finset +import Mathlib.Tactic.Linarith + +/-! +# The closed form of Ruzsa's bound + +For `1 ≤ m ≤ n` the sum `∑ t ∈ {1, …, m - 1}, min d (n - t)` is at least +`d * m - d * (d + 1) / 2`. With Ruzsa's theorem this gives the asymmetric form of Freiman's lemma: +if `A, B ⊆ ℝ^D` are finite sets with `B` nonempty and `|B| ≤ |A|`, and `d` is at most the affine +dimension of `A + B`, then `|A + B| ≥ |A| + d * |B| - d * (d + 1) / 2`. + +## Main statements + +* `card_add_mul_card_le_card_add_add`: the bound, as `|A| + d * |B| ≤ |A + B| + d * (d + 1) / 2` + in `ℕ`. +* `card_add_mul_card_le_card_add_add_of_le_finrank_span_sub`: the same bound, with the affine + dimension written as the dimension of the span of `(A + B) - (A + B)`. +* `two_mul_card_add_mul_card_le`: the same bound multiplied by two, without division. +* `card_add_mul_card_sub_le_card_add`: the same bound in `ℝ`. +* `max_card_add_mul_min_card_le_card_add_add`: the bound without the assumption `|B| ≤ |A|`, with + the larger and the smaller of `|A|` and `|B|` in place of `|A|` and `|B|`. +-/ + +public section + +namespace SumOfSetsInSeveralDimensions + +open Finset +open scoped Pointwise + +private lemma sum_min_add_le {d k n : ℕ} (hkn : k + 2 ≤ n) : + ∑ t ∈ Icc 1 k, min d (n - 1 - t) + (k + 1) ≤ ∑ t ∈ Icc 1 (k + 1), min (d + 1) (n - t) := by + have h : ∑ t ∈ Icc 1 k, (min d (n - 1 - t) + 1) ≤ ∑ t ∈ Icc 1 k, min (d + 1) (n - t) := by + apply sum_le_sum + grind + rw [sum_add_distrib, sum_const, Nat.card_Icc, smul_eq_mul] at h + rw [sum_Icc_succ_top (by grind)] + grind + +private lemma two_mul_mul_succ_le {k d n : ℕ} (hn : k + 1 ≤ n) : + 2 * (d * (k + 1)) ≤ 2 * ∑ t ∈ Icc 1 k, min d (n - t) + d * (d + 1) := by + induction k generalizing d n with + | zero => grind [Nat.le_mul_self d] + | succ k ih => + obtain _ | d := d + · simp + · grind [ih (d := d) (n := n - 1) (by grind), sum_min_add_le (d := d) hn] + +/-- For `1 ≤ m ≤ n`, twice the sum `∑ t ∈ {1, …, m - 1}, min d (n - t)` is at least +`2 * d * m - d * (d + 1)`. -/ +lemma two_mul_mul_le_two_mul_sum_min_add (d : ℕ) {m n : ℕ} (hm : 1 ≤ m) (hmn : m ≤ n) : + 2 * (d * m) ≤ 2 * ∑ t ∈ Icc 1 (m - 1), min d (n - t) + d * (d + 1) := by + obtain ⟨k, rfl⟩ := Nat.exists_eq_add_one.2 hm + exact two_mul_mul_succ_le hmn + +variable {D d : ℕ} {A B : Finset (Fin D → ℝ)} + +/-- The closed form of Ruzsa's bound, multiplied by two: `2 * (|A| + d * |B|)` is at most +`2 * |A + B| + d * (d + 1)`. -/ +lemma two_mul_card_add_mul_card_le (hB : B.Nonempty) (hBA : #B ≤ #A) + (hd : d ≤ (A + B).affineDim) : 2 * (#A + d * #B) ≤ 2 * #(A + B) + d * (d + 1) := by + grind [card_add_sum_min_le_card_add_of_le hB hBA hd, + two_mul_mul_le_two_mul_sum_min_add d hB.card_pos hBA] + +/-- **The asymmetric form of Freiman's lemma.** If `A, B ⊆ ℝ^D` are finite, `B` is nonempty, +`|B| ≤ |A|` and `A + B` has affine dimension at least `d`, then +`|A| + d * |B| ≤ |A + B| + d * (d + 1) / 2`. -/ +theorem card_add_mul_card_le_card_add_add (hB : B.Nonempty) (hBA : #B ≤ #A) + (hd : d ≤ (A + B).affineDim) : + #A + d * #B ≤ #(A + B) + d * (d + 1) / 2 := by + grind [two_mul_card_add_mul_card_le hB hBA hd] + +/-- The asymmetric form of Freiman's lemma, with the affine dimension of `A + B` written as the +dimension of the span of `(A + B) - (A + B)`. -/ +theorem card_add_mul_card_le_card_add_add_of_le_finrank_span_sub (hB : B.Nonempty) + (hBA : #B ≤ #A) + (hd : d ≤ Module.finrank ℝ (Submodule.span ℝ (↑(A + B) - ↑(A + B) : Set (Fin D → ℝ)))) : + #A + d * #B ≤ #(A + B) + d * (d + 1) / 2 := + card_add_mul_card_le_card_add_add hB hBA + (hd.trans_eq (affineDim_eq_finrank_span_sub _).symm) + +/-- The asymmetric form of Freiman's lemma in `ℝ`: `|A| + d * |B| - d * (d + 1) / 2 ≤ |A + B|`. -/ +lemma card_add_mul_card_sub_le_card_add (hB : B.Nonempty) (hBA : #B ≤ #A) + (hd : d ≤ (A + B).affineDim) : + (#A : ℝ) + d * #B - d * (d + 1) / 2 ≤ #(A + B) := by + have h : (2 * (#A + d * #B) : ℝ) ≤ 2 * #(A + B) + d * (d + 1) := + mod_cast two_mul_card_add_mul_card_le hB hBA hd + linarith + +/-- The asymmetric form of Freiman's lemma without an assumption on which set is larger. -/ +lemma max_card_add_mul_min_card_le_card_add_add (hA : A.Nonempty) (hB : B.Nonempty) + (hd : d ≤ (A + B).affineDim) : + max #A #B + d * min #A #B ≤ #(A + B) + d * (d + 1) / 2 := by + rcases le_total #B #A with h | h + · rw [max_eq_left h, min_eq_right h] + exact card_add_mul_card_le_card_add_add hB h hd + · rw [max_eq_right h, min_eq_left h, add_comm A B] + exact card_add_mul_card_le_card_add_add hA h (add_comm A B ▸ hd) + +end SumOfSetsInSeveralDimensions diff --git a/LeanPool/SumOfSetsInSeveralDimensions/Construction.lean b/LeanPool/SumOfSetsInSeveralDimensions/Construction.lean new file mode 100644 index 0000000000..139d1929d6 --- /dev/null +++ b/LeanPool/SumOfSetsInSeveralDimensions/Construction.lean @@ -0,0 +1,237 @@ +/- +Copyright (c) 2026 Gabriel Dahia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Dahia +-/ +module + +public import LeanPool.SumOfSetsInSeveralDimensions.AffineDim +public import LeanPool.SumOfSetsInSeveralDimensions.LowerBoundFunction +public import Mathlib.Algebra.Group.Pointwise.Finset.Basic +import Mathlib.Data.Finset.Sym +import Mathlib.Data.Fintype.Fin +import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional +import Mathlib.LinearAlgebra.StdBasis +import Mathlib.Tactic.Linarith +import LeanPool.SumOfSetsInSeveralDimensions.AffineDimSumset +import LeanPool.SumOfSetsInSeveralDimensions.LowerBound +import LeanPool.SumOfSetsInSeveralDimensions.LowerBoundValues + +/-! +# Sets with a small sumset + +Section 3 of Ruzsa's paper. Let `e₀, …, e_(d-1)` be the unit vectors of `ℝ^d`, let `1 ≤ m ≤ n` +and `n ≥ d + 1`, and put `t = n - m` and `c = d - 1 - t` when `t < d - 1`, `c = 0` otherwise. The +sets + +* `B = {0, e₀, …, (n - d) e₀} ∪ {e₁, …, e_(d-1)}`, +* `A = {0, e₀, …, (m - 1 - c) e₀} ∪ {e₁, …, e_c}` + +have `|A| = m`, `|B| = n`, `B` has affine dimension `d`, and `|A + B| = G_d(m, n)`. With +Ruzsa's theorem, this shows that `G_d(m, n)` is the least size of such a sumset. + +The paper takes `A = {0, e₀, …, (m - 1) e₀}` when `t ≥ d`, which is the case `c = 0`. Its count +of `|A + B|` when `t < d` lists the sums `e_i + e_j` with `i, j ≤ c`, but the sums with `i ≤ c` +and `c < j` also occur; its final value `G_d(m, n)` is correct. + +## Main definitions + +* `axisUnionBasis e k c`: the set `{0, e₀, …, k e₀} ∪ {e₁, …, e_c}` in `ℝ^(e + 1)`. + +## Main statements + +* `exists_card_add_eq_sumsetCardLowerBound`: for `1 ≤ d`, `1 ≤ m ≤ n` and `d + 1 ≤ n`, there are + `A, B ⊆ ℝ^d` with `|A| = m`, `|B| = n`, `B` of affine dimension `d` and `|A + B| = G_d(m, n)`. +-/ + +public section + +namespace SumOfSetsInSeveralDimensions + +open Finset +open scoped Pointwise + +variable {e : ℕ} + +/-- The points `i e₀` of `ℝ^(e + 1)` with `i ≤ k`. -/ +noncomputable def axisPoints (e k : ℕ) : Finset (Fin (e + 1) → ℝ) := + (range (k + 1)).image fun i : ℕ ↦ Pi.single 0 (i : ℝ) + +/-- The unit vectors `e_(j + 1)` of `ℝ^(e + 1)` with `j < c`. -/ +noncomputable def unitVectors (e c : ℕ) : Finset (Fin (e + 1) → ℝ) := + ({j : Fin e | (j : ℕ) < c} : Finset (Fin e)).image fun j ↦ Pi.single j.succ 1 + +/-- The set `{0, e₀, …, k e₀} ∪ {e₁, …, e_c}` of `ℝ^(e + 1)`. -/ +noncomputable def axisUnionBasis (e k c : ℕ) : Finset (Fin (e + 1) → ℝ) := + axisPoints e k ∪ unitVectors e c + +lemma card_axisPoints (e k : ℕ) : #(axisPoints e k) = k + 1 := by + rw [axisPoints, card_image_of_injective, card_range] + intro a b h + simpa using congr_fun h 0 + +lemma card_unitVectors {c : ℕ} (hc : c ≤ e) : #(unitVectors e c) = c := by + rw [unitVectors, card_image_of_injective, Fin.card_filter_val_lt, min_eq_right hc] + intro i j h + simpa [Pi.single_apply] using congr_fun h i.succ + +lemma disjoint_axisPoints_unitVectors (k c : ℕ) : + Disjoint (axisPoints e k) (unitVectors e c) := by + rw [disjoint_left] + intro x hx hx' + obtain ⟨i, -, rfl⟩ := mem_image.1 hx + obtain ⟨j, -, h⟩ := mem_image.1 hx' + simpa using congr_fun h j.succ + +lemma card_axisUnionBasis (k : ℕ) {c : ℕ} (hc : c ≤ e) : #(axisUnionBasis e k c) = k + 1 + c := by + rw [axisUnionBasis, card_union_of_disjoint (disjoint_axisPoints_unitVectors k c), + card_axisPoints, card_unitVectors hc] + +lemma axisPoints_mono {k l : ℕ} (hkl : k ≤ l) : axisPoints e k ⊆ axisPoints e l := by + apply image_subset_image + grind + +lemma unitVectors_mono {c c' : ℕ} (hcc' : c ≤ c') : unitVectors e c ⊆ unitVectors e c' := by + apply image_subset_image + intro j + simp only [mem_filter, mem_univ, true_and] + grind + +lemma axisPoints_add_axisPoints_subset (k l : ℕ) : + axisPoints e k + axisPoints e l ⊆ axisPoints e (k + l) := by + intro z hz + obtain ⟨_, hx, _, hy, rfl⟩ := mem_add.1 hz + obtain ⟨i, hi, rfl⟩ := mem_image.1 hx + obtain ⟨j, hj, rfl⟩ := mem_image.1 hy + refine mem_image.2 ⟨i + j, by grind, ?_⟩ + rw [Nat.cast_add, Pi.single_add] + +/-- The set `axisUnionBasis e k e` contains `0`, `e₀` and all of `e₁, …, e_e`, so it has affine +dimension `e + 1` when `k ≥ 1`. -/ +lemma affineDim_axisUnionBasis {k : ℕ} (hk : 1 ≤ k) : + (axisUnionBasis e k e).affineDim = e + 1 := by + have h0 : (0 : Fin (e + 1) → ℝ) ∈ axisUnionBasis e k e := + mem_union_left _ (mem_image.2 ⟨0, by simp, by simp⟩) + suffices h : Submodule.span ℝ + ((· -ᵥ (0 : Fin (e + 1) → ℝ)) '' (axisUnionBasis e k e : Set (Fin (e + 1) → ℝ))) = ⊤ by + rw [affineDim_eq_finrank_vectorSpan, vectorSpan_eq_span_vsub_set_right ℝ (mem_coe.2 h0), + h, finrank_top, Module.finrank_fin_fun] + rw [eq_top_iff, ← (Pi.basisFun ℝ (Fin (e + 1))).span_eq, Submodule.span_le] + rintro _ ⟨i, rfl⟩ + apply Submodule.subset_span + refine ⟨Pi.single i 1, ?_, by simp⟩ + induction i using Fin.cases with + | zero => exact mem_union_left _ (mem_image.2 ⟨1, by grind, by simp⟩) + | succ j => exact mem_union_right _ (mem_image.2 ⟨j, by simp, rfl⟩) + +private lemma card_add_self_le {α : Type*} [AddCommMonoid α] [DecidableEq α] (S : Finset α) : + #(S + S) ≤ (#S + 1).choose 2 := by + rw [← card_sym2] + refine (card_le_card ?_).trans (card_image_le (f := Sym2.lift ⟨(· + ·), add_comm⟩)) + intro z hz + obtain ⟨a, ha, b, hb, rfl⟩ := mem_add.1 hz + exact mem_image.2 ⟨s(a, b), mk_mem_sym2_iff.2 ⟨ha, hb⟩, rfl⟩ + +private lemma card_unitVectors_add_le {c : ℕ} (hc : c ≤ e) : + #(unitVectors e c + unitVectors e e) ≤ (c + 1).choose 2 + c * (e - c) := by + have hsub : unitVectors e c + unitVectors e e ⊆ (unitVectors e c + unitVectors e c) ∪ + (unitVectors e c + (unitVectors e e \ unitVectors e c)) := by + intro z hz + obtain ⟨a, ha, b, hb, rfl⟩ := mem_add.1 hz + by_cases hbc : b ∈ unitVectors e c + · exact mem_union_left _ (add_mem_add ha hbc) + · exact mem_union_right _ (add_mem_add ha (mem_sdiff.2 ⟨hb, hbc⟩)) + refine (card_le_card hsub).trans ((card_union_le _ _).trans (add_le_add ?_ ?_)) + · simpa [card_unitVectors hc] using card_add_self_le (unitVectors e c) + · refine card_add_le.trans_eq ?_ + rw [card_sdiff_of_subset (unitVectors_mono hc), card_unitVectors hc, card_unitVectors le_rfl] + +/-- If `c = 0` or `p ≤ q`, then the sum of `{0, …, q e₀} ∪ {e₁, …, e_c}` and +`{0, …, p e₀} ∪ {e₁, …, e_e}` lies in `{0, …, (p + q) e₀} ∪ ({0, …, q e₀} + {e₁, …, e_e}) ∪ +({e₁, …, e_c} + {e₁, …, e_e})`. -/ +private lemma axisUnionBasis_add_axisUnionBasis_subset {p q c : ℕ} (hcq : c = 0 ∨ p ≤ q) + (hc : c ≤ e) : + axisUnionBasis e q c + axisUnionBasis e p e ⊆ axisPoints e (q + p) ∪ + (axisPoints e q + unitVectors e e) ∪ (unitVectors e c + unitVectors e e) := by + intro z hz + obtain ⟨a, ha, b, hb, rfl⟩ := mem_add.1 hz + simp only [mem_union] + obtain ha | ha := mem_union.1 ha <;> obtain hb | hb := mem_union.1 hb + · exact Or.inl (Or.inl (axisPoints_add_axisPoints_subset q p (add_mem_add ha hb))) + · exact Or.inl (Or.inr (add_mem_add ha hb)) + · obtain rfl | hpq := hcq + · simp [unitVectors] at ha + · rw [add_comm a b] + exact Or.inl (Or.inr (add_mem_add (axisPoints_mono hpq hb) (unitVectors_mono hc ha))) + · exact Or.inr (add_mem_add ha hb) + +private lemma card_axisUnionBasis_add_le {p q c : ℕ} (hcq : c = 0 ∨ p ≤ q) (hc : c ≤ e) : + #(axisUnionBasis e q c + axisUnionBasis e p e) ≤ + q + p + 1 + (q + 1) * e + (c + 1).choose 2 + c * (e - c) := by + grind [card_le_card (axisUnionBasis_add_axisUnionBasis_subset hcq hc), + card_union_le (axisPoints e (q + p) ∪ (axisPoints e q + unitVectors e e)) + (unitVectors e c + unitVectors e e), + card_union_le (axisPoints e (q + p)) (axisPoints e q + unitVectors e e), + card_add_le (s := axisPoints e q) (t := unitVectors e e), card_axisPoints e (q + p), + card_axisPoints e q, card_unitVectors (e := e) le_rfl, card_unitVectors_add_le hc] + +private lemma two_mul_choose_two_add_one (c : ℕ) : 2 * (c + 1).choose 2 = (c + 1) * c := by + rw [Nat.choose_two_right, Nat.add_sub_cancel, mul_comm (c + 1), + Nat.two_mul_div_two_of_even (Nat.even_mul_succ_self c)] + +/-- The construction when `t = n - m ≥ e`: `A = {0, e₀, …, (m - 1) e₀}`. -/ +private lemma exists_card_add_le_of_le {m n : ℕ} (hm : 1 ≤ m) (hn : e + 2 ≤ n) (hmn : m + e ≤ n) : + ∃ A B : Finset (Fin (e + 1) → ℝ), #A = m ∧ #B = n ∧ B.affineDim = e + 1 ∧ + #(A + B) ≤ sumsetCardLowerBound (e + 1) m n := by + obtain ⟨a, rfl⟩ := Nat.exists_eq_add_of_le' hm + obtain ⟨r, rfl⟩ := Nat.exists_eq_add_of_le hmn + refine ⟨axisUnionBasis e a 0, axisUnionBasis e (a + r) e, by simp [card_axisUnionBasis], + by rw [card_axisUnionBasis _ le_rfl]; grind, affineDim_axisUnionBasis (by grind), ?_⟩ + rw [sumsetCardLowerBound_of_add_le (by grind), Nat.add_sub_cancel] + grind [card_axisUnionBasis_add_le (e := e) (p := a + r) (q := a) (Or.inl rfl) (Nat.zero_le e), + Nat.choose_eq_zero_of_lt (by grind : 0 + 1 < 2)] + +/-- The construction when `t = n - m < e`: with `c = e - t`, `A = {0, …, p e₀} ∪ {e₁, …, e_c}` +and `B = {0, …, p e₀} ∪ {e₁, …, e_e}` for `p = n - 1 - e`. -/ +private lemma exists_card_add_le_of_lt {m n : ℕ} (hmn : m ≤ n) (hn : e + 2 ≤ n) (hnm : n < m + e) : + ∃ A B : Finset (Fin (e + 1) → ℝ), #A = m ∧ #B = n ∧ B.affineDim = e + 1 ∧ + #(A + B) ≤ sumsetCardLowerBound (e + 1) m n := by + obtain ⟨t, rfl⟩ := Nat.exists_eq_add_of_le hmn + obtain ⟨c, rfl⟩ := Nat.exists_eq_add_of_lt (by grind : t < e) + obtain ⟨p, rfl⟩ := Nat.exists_eq_add_of_le (by grind : c + 2 ≤ m) + refine ⟨axisUnionBasis (t + c + 1) p (c + 1), axisUnionBasis (t + c + 1) p (t + c + 1), + by rw [card_axisUnionBasis _ (by grind)]; grind, + by rw [card_axisUnionBasis _ le_rfl]; grind, affineDim_axisUnionBasis (by grind), ?_⟩ + have h := two_mul_sumsetCardLowerBound_add_add (d := t + c + 1 + 1) (m := c + 2 + p) + (n := c + 2 + p + t) (by grind) (by grind) (by grind) + rw [Nat.add_sub_cancel_left] at h + apply (card_axisUnionBasis_add_le (Or.inr le_rfl) (by grind)).trans + rw [(by grind : t + c + 1 - (c + 1) = t)] + nlinarith [two_mul_choose_two_add_one (c + 1)] + +/-- For `1 ≤ m ≤ n` and `e + 2 ≤ n`, there are `A, B ⊆ ℝ^(e + 1)` with `|A| = m`, `|B| = n`, `B` +of affine dimension `e + 1` and `|A + B| ≤ G_(e + 1)(m, n)`. -/ +lemma exists_card_add_le_sumsetCardLowerBound {m n : ℕ} (hm : 1 ≤ m) (hmn : m ≤ n) + (hn : e + 2 ≤ n) : + ∃ A B : Finset (Fin (e + 1) → ℝ), #A = m ∧ #B = n ∧ B.affineDim = e + 1 ∧ + #(A + B) ≤ sumsetCardLowerBound (e + 1) m n := by + obtain hmn' | hnm := le_or_gt (m + e) n + · exact exists_card_add_le_of_le hm hn hmn' + · exact exists_card_add_le_of_lt hmn hn hnm + +/-- **The sets of Section 3.** For `1 ≤ d`, `1 ≤ m ≤ n` and `d + 1 ≤ n`, there are `A, B ⊆ ℝ^d` +with `|A| = m`, `|B| = n`, `B` of affine dimension `d` and +`|A + B| = n + ∑ j ∈ {1, …, m - 1}, min d (n - j)`. -/ +theorem exists_card_add_eq_sumsetCardLowerBound {d m n : ℕ} (hd : 1 ≤ d) (hm : 1 ≤ m) + (hmn : m ≤ n) (hn : d + 1 ≤ n) : + ∃ A B : Finset (Fin d → ℝ), #A = m ∧ #B = n ∧ B.affineDim = d ∧ + #(A + B) = sumsetCardLowerBound d m n := by + obtain ⟨e, rfl⟩ := Nat.exists_eq_add_of_le' hd + obtain ⟨A, B, hA, hB, hBdim, hAB⟩ := exists_card_add_le_sumsetCardLowerBound hm hmn hn + refine ⟨A, B, hA, hB, hBdim, le_antisymm hAB ?_⟩ + have hA' : A.Nonempty := card_pos.1 (by grind) + have h := card_add_sum_min_le_card_add (A := B) (B := A) hA' (by grind) + (affineDim_add_eq_of_left_eq hA' hBdim) + rwa [add_comm B, hA, hB, ← sumsetCardLowerBound_eq] at h + +end SumOfSetsInSeveralDimensions diff --git a/LeanPool/SumOfSetsInSeveralDimensions/FreimanDimension.lean b/LeanPool/SumOfSetsInSeveralDimensions/FreimanDimension.lean new file mode 100644 index 0000000000..24cbd2dc05 --- /dev/null +++ b/LeanPool/SumOfSetsInSeveralDimensions/FreimanDimension.lean @@ -0,0 +1,69 @@ +/- +Copyright (c) 2026 Gabriel Dahia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Dahia +-/ +module + +public import Mathlib.Combinatorics.Additive.FreimanHom +public import LeanPool.SumOfSetsInSeveralDimensions.AffineDim + +/-! +# The Freiman dimension + +The Freiman dimension of a finite subset `X` of an abelian group is the largest `d ≤ |X|` such that +`X` is Freiman isomorphic of order `2` to a subset of `ℚ^d` that is not contained in a proper +affine subspace. The affine dimension of the image is the `Finset.affineDim` of its inclusion in +`ℝ^d`. + +## Main definitions + +* `rationalVectorToReal`: the coordinatewise inclusion of `ℚ^d` into `ℝ^d`. +* `freimanModelDim X d`: `X` is Freiman isomorphic to a subset of `ℚ^d` of affine dimension `d`. +* `freimanDim X`: the Freiman dimension of `X`. + +## Main statements + +* `le_freimanDim_of_model`: if `d ≤ |X|` and `freimanModelDim X d`, then `d ≤ freimanDim X`. +* `freimanDim_add_one_le_card`: a nonempty set `X` has Freiman dimension at most `|X| - 1`. +-/ + +@[expose] public section + +namespace SumOfSetsInSeveralDimensions + +open Finset + +/-- The coordinatewise inclusion of rational vectors into real vectors. -/ +def rationalVectorToReal {d : ℕ} (v : Fin d → ℚ) : Fin d → ℝ := fun i ↦ (v i : ℝ) + +/-- The set `X` has a Freiman model of dimension `d`: there is a Freiman isomorphism of order `2` +from `X` onto a subset of `ℚ^d` of affine dimension `d`. -/ +def freimanModelDim {G : Type*} [AddCommMonoid G] (X : Finset G) (d : ℕ) : Prop := + ∃ f : G → (Fin d → ℚ), IsAddFreimanIso 2 (X : Set G) (X.image f : Set (Fin d → ℚ)) f ∧ + ((X.image f).image rationalVectorToReal).affineDim = d + +/-- The Freiman dimension of `X`: the largest `d ≤ |X|` such that `X` has a Freiman model of +dimension `d`. -/ +noncomputable def freimanDim {G : Type*} [AddCommMonoid G] (X : Finset G) : ℕ := by + classical + exact Nat.findGreatest (freimanModelDim X) #X + +/-- A Freiman model of `X` of dimension `d ≤ |X|` shows that `d ≤ freimanDim X`. -/ +lemma le_freimanDim_of_model {G : Type*} [AddCommMonoid G] {X : Finset G} {d : ℕ} + (hd : d ≤ #X) (hmodel : freimanModelDim X d) : d ≤ freimanDim X := by + classical + exact Nat.le_findGreatest hd hmodel + +/-- A nonempty set `X` has Freiman dimension at most `|X| - 1`. -/ +lemma freimanDim_add_one_le_card {G : Type*} [AddCommMonoid G] {X : Finset G} + (hX : X.Nonempty) : freimanDim X + 1 ≤ #X := by + classical + by_cases h : freimanDim X = 0 + · grind [hX.card_pos] + obtain ⟨f, -, hdim⟩ : freimanModelDim X (freimanDim X) := Nat.findGreatest_of_ne_zero rfl h + grind [affineDim_add_one_le_card ((hX.image f).image rationalVectorToReal), + card_image_le (s := X) (f := f), + card_image_le (s := X.image f) (f := rationalVectorToReal)] + +end SumOfSetsInSeveralDimensions diff --git a/LeanPool/SumOfSetsInSeveralDimensions/FreimanDimensionSumsetBounds.lean b/LeanPool/SumOfSetsInSeveralDimensions/FreimanDimensionSumsetBounds.lean new file mode 100644 index 0000000000..71dc60a982 --- /dev/null +++ b/LeanPool/SumOfSetsInSeveralDimensions/FreimanDimensionSumsetBounds.lean @@ -0,0 +1,326 @@ +/- +Copyright (c) 2026 Gabriel Dahia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Dahia +-/ +module + +public import Mathlib.Algebra.Group.Pointwise.Finset.Basic +public import LeanPool.SumOfSetsInSeveralDimensions.FreimanDimension +import Mathlib.Algebra.BigOperators.Intervals +import Mathlib.Algebra.Order.Interval.Finset.SuccPred +import Mathlib.Data.Nat.Choose.Cast +import Mathlib.Data.Nat.Choose.Sum +import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas +import Mathlib.Tactic.Linarith +import LeanPool.SumOfSetsInSeveralDimensions.AffineDimSumset +import LeanPool.SumOfSetsInSeveralDimensions.ClosedForm +import LeanPool.SumOfSetsInSeveralDimensions.LowerBound + +/-! +# Sumset bounds from the Freiman dimension + +Let `A` and `B` be finite subsets of a commutative monoid with `B` nonempty and `|B| ≤ |A|`, and +let `f` be a Freiman isomorphism of order `2` from `A ∪ B` onto a subset of `ℝ^r` of affine +dimension `r`. Then `f` sends `A` and `B` to sets `A'` and `B'` with `|A'| = |A|`, `|B'| = |B|` and +`|A' + B'| = |A + B|`, and `A' + B'` has affine dimension at least `r - 1`. Ruzsa's theorem then +gives `|A| + ∑ t ∈ {1, …, |B| - 1}, min (r - 1) (|A| - t) ≤ |A + B|`. A Freiman model in `ℚ^r` is +one in `ℝ^r`, so this holds when `r ≥ 1` is the Freiman dimension of `A ∪ B`. + +For `A = B = X` the model `f(X) + f(X)` has affine dimension `r`, and the asymmetric form of +Freiman's lemma gives `(r + 1) * |X| - r * (r + 1) / 2 ≤ |X + X|`. If `|X + X| ≤ κ * |X|`, then +`r ≤ 2 * κ - 1`, so `r * (r + 1) / 2 ≤ κ * (2 * κ - 1)` and `r ≤ κ - 1 + κ * (2 * κ - 1) / |X|`. + +## Main statements + +* `card_add_sum_min_le_card_add_of_isAddFreimanIso`: the bound above. +* `card_add_sum_min_le_of_freimanDim_union`: the bound for `r` the Freiman dimension of `A ∪ B`. +* `two_mul_card_add_mul_card_le_of_isAddFreimanIso`: Freiman's lemma for a Freiman model `f` of + `X` in `ℝ^r` of affine dimension `r`, `2 * (|X| + r * |X|) ≤ 2 * |X + X| + r * (r + 1)`. +* `card_add_mul_card_sub_choose_le_card_add_of_freimanDim_union`: the weaker bound + `|A| + (r - 1) * |B| - (r + 1).choose 2 ≤ |A + B|`. +* `card_add_mul_card_sub_le_card_add_of_freimanDim`: if `X` is nonempty with Freiman dimension + `r ≥ 1`, then `|X| + r * |X| - r * (r + 1) / 2 ≤ |X + X|`. +* `le_two_mul_sub_one_of_isAddFreimanIso`: if `|X + X| ≤ κ * |X|` for a real `κ`, then a Freiman + model of `X` in `ℝ^r` of affine dimension `r` has `r ≤ 2 * κ - 1`. +* `freimanDim_le_two_mul_sub_one_of_card_add_le`: if `|X + X| ≤ κ * |X|`, then + `freimanDim X ≤ 2 * κ - 1`. +* `le_sub_one_add_mul_div_card_of_isAddFreimanIso`: under the same hypotheses, + `r ≤ κ - 1 + κ * (2 * κ - 1) / |X|`. +* `freimanDim_le_sub_one_add_mul_div_card_of_card_add_le`: if `|X + X| ≤ κ * |X|`, then + `freimanDim X ≤ κ - 1 + κ * (2 * κ - 1) / |X|`. +-/ + +@[expose] public section + +namespace SumOfSetsInSeveralDimensions + +open Finset +open scoped Pointwise + +noncomputable section + +lemma rationalVectorToReal_injective {d : ℕ} : + Function.Injective (rationalVectorToReal (d := d)) := + Rat.cast_injective.comp_left + +lemma rationalVectorToReal_add {d : ℕ} (x y : Fin d → ℚ) : + rationalVectorToReal (x + y) = rationalVectorToReal x + rationalVectorToReal y := by + ext i + simp [rationalVectorToReal] + +/-- A Freiman isomorphism into `ℚ^d` followed by the inclusion of `ℚ^d` into `ℝ^d` is a Freiman +isomorphism into `ℝ^d`. -/ +lemma isAddFreimanIso_rationalVectorToReal_comp {G : Type*} [AddCommMonoid G] {d : ℕ} + {X : Finset G} {f : G → (Fin d → ℚ)} + (hf : IsAddFreimanIso 2 (X : Set G) (X.image f : Set (Fin d → ℚ)) f) : + IsAddFreimanIso 2 (X : Set G) (X.image (rationalVectorToReal ∘ f) : Set (Fin d → ℝ)) + (rationalVectorToReal ∘ f) := by + rw [isAddFreimanIso_two] at hf ⊢ + constructor + · rw [coe_image] + exact (rationalVectorToReal_injective.comp_injOn hf.1.injOn).bijOn_image + · intro a ha b hb c hc e he + simp only [Function.comp, ← rationalVectorToReal_add, rationalVectorToReal_injective.eq_iff] + exact hf.2 a ha b hb c hc e he + +/-- A set of Freiman dimension `r ≥ 1` has a Freiman model in `ℝ^r` of affine dimension `r`. -/ +lemma exists_isAddFreimanIso_of_freimanDim_eq {G : Type*} [AddCommMonoid G] + {r : ℕ} {X : Finset G} (hdim : freimanDim X = r) (hr : r ≠ 0) : + ∃ f : G → Fin r → ℝ, IsAddFreimanIso 2 (X : Set G) (X.image f : Set (Fin r → ℝ)) f ∧ + (X.image f).affineDim = r := by + classical + obtain ⟨f, hf, haff⟩ := Nat.findGreatest_of_ne_zero hdim hr + exact ⟨_, isAddFreimanIso_rationalVectorToReal_comp hf, by rwa [← image_image]⟩ + +/-- Two maps with the same fibres on `s` have images of `s` of the same size. -/ +lemma card_image_eq_of_kernel_iff {α β γ : Type*} [DecidableEq β] [DecidableEq γ] + {s : Finset α} {f : α → β} {g : α → γ} + (h : ∀ x ∈ s, ∀ y ∈ s, (f x = f y ↔ g x = g y)) : + #(s.image f) = #(s.image g) := by + apply card_bij (fun b hb ↦ g (mem_image.mp hb).choose) + · intro b hb + exact mem_image_of_mem g (mem_image.mp hb).choose_spec.1 + · intro b₁ hb₁ b₂ hb₂ hgb + obtain ⟨hx₁, hfb₁⟩ := (mem_image.mp hb₁).choose_spec + obtain ⟨hx₂, hfb₂⟩ := (mem_image.mp hb₂).choose_spec + exact hfb₁ ▸ hfb₂ ▸ (h _ hx₁ _ hx₂).2 hgb + · intro c hc + obtain ⟨x, hx, rfl⟩ := mem_image.mp hc + obtain ⟨hy, hfy⟩ := (mem_image.mp (mem_image_of_mem f hx)).choose_spec + exact ⟨f x, mem_image_of_mem f hx, (h _ hy _ hx).1 hfy⟩ + +/-- A Freiman isomorphism of order `2` on `X` preserves the size of `A + B` for `A, B ⊆ X`. -/ +lemma card_add_image_of_isAddFreimanIso {G H : Type*} [DecidableEq G] [DecidableEq H] + [AddCommMonoid G] [AddCommMonoid H] {X A B : Finset G} {f : G → H} + (hf : IsAddFreimanIso 2 (X : Set G) (X.image f : Set H) f) (hAX : A ⊆ X) (hBX : B ⊆ X) : + #(A.image f + B.image f) = #(A + B) := by + rw [add_def, add_def, ← prodMap_image_product, image_image] + apply card_image_eq_of_kernel_iff + rintro ⟨a, b⟩ hab ⟨a', b'⟩ hab' + obtain ⟨ha, hb⟩ := mem_product.1 hab + obtain ⟨ha', hb'⟩ := mem_product.1 hab' + exact hf.add_eq_add (hAX ha) (hBX hb) (hAX ha') (hBX hb') + +/-- **Ruzsa's theorem for a Freiman model.** Let `A` and `B` be finite subsets of a commutative +monoid with `B` nonempty and `|B| ≤ |A|`, and let `f` be a Freiman isomorphism of order `2` from +`A ∪ B` onto a subset of `ℝ^r` of affine dimension `r`. Then +`|A| + ∑ t ∈ {1, …, |B| - 1}, min (r - 1) (|A| - t) ≤ |A + B|`. -/ +theorem card_add_sum_min_le_card_add_of_isAddFreimanIso {G : Type*} [DecidableEq G] + [AddCommMonoid G] {r : ℕ} {A B : Finset G} {f : G → Fin r → ℝ} (hB : B.Nonempty) + (hBA : #B ≤ #A) + (hf : IsAddFreimanIso 2 ((A ∪ B : Finset G) : Set G) ((A ∪ B).image f : Set (Fin r → ℝ)) f) + (hdim : ((A ∪ B).image f).affineDim = r) : + #A + ∑ t ∈ Icc 1 (#B - 1), min (r - 1) (#A - t) ≤ #(A + B) := by + have hcard {S : Finset G} (hS : S ⊆ A ∪ B) : #(S.image f) = #S := + card_image_of_injOn (hf.bijOn.injOn.mono (coe_subset.2 hS)) + have hA : A.Nonempty := card_pos.1 (hB.card_pos.trans_le hBA) + have h := card_add_sum_min_le_card_add_of_le (d := r - 1) (hB.image f) + (by rwa [hcard subset_union_left, hcard subset_union_right]) + (by grind [image_union, affineDim_union_le_sum_add_one (hA.image f) (hB.image f)]) + rwa [hcard subset_union_left, hcard subset_union_right, + card_add_image_of_isAddFreimanIso hf subset_union_left subset_union_right] at h + +/-- Ruzsa's theorem for a Freiman model, with the affine dimension of the model written as the +dimension of the span of its differences. -/ +theorem card_add_sum_min_le_card_add_of_isAddFreimanIso_of_finrank_span_sub_eq {G : Type*} + [DecidableEq G] [AddCommMonoid G] {r : ℕ} {A B : Finset G} {f : G → Fin r → ℝ} + (hB : B.Nonempty) (hBA : #B ≤ #A) + (hf : IsAddFreimanIso 2 ((A ∪ B : Finset G) : Set G) ((A ∪ B).image f : Set (Fin r → ℝ)) f) + (hdim : Module.finrank ℝ (Submodule.span ℝ + (↑((A ∪ B).image f) - ↑((A ∪ B).image f) : Set (Fin r → ℝ))) = r) : + #A + ∑ t ∈ Icc 1 (#B - 1), min (r - 1) (#A - t) ≤ #(A + B) := + card_add_sum_min_le_card_add_of_isAddFreimanIso hB hBA hf + ((affineDim_eq_finrank_span_sub _).trans hdim) + +/-- **Freiman's lemma for a Freiman model.** If `f` is a Freiman isomorphism of order `2` from a +nonempty `X` onto a subset of `ℝ^r` of affine dimension `r`, then +`2 * (|X| + r * |X|) ≤ 2 * |X + X| + r * (r + 1)`. -/ +lemma two_mul_card_add_mul_card_le_of_isAddFreimanIso {G : Type*} [DecidableEq G] + [AddCommMonoid G] {r : ℕ} {X : Finset G} {f : G → Fin r → ℝ} (hX : X.Nonempty) + (hf : IsAddFreimanIso 2 (X : Set G) (X.image f : Set (Fin r → ℝ)) f) + (hdim : (X.image f).affineDim = r) : + 2 * (#X + r * #X) ≤ 2 * #(X + X) + r * (r + 1) := by + have h := two_mul_card_add_mul_card_le (hX.image f) le_rfl + (hdim.symm.trans_le (affineDim_le_affineDim_add_right _ (hX.image f))) + rwa [card_image_of_injOn hf.bijOn.injOn, + card_add_image_of_isAddFreimanIso hf subset_rfl subset_rfl] at h + +private lemma sub_one_mul_le_choose_add_choose (b r : ℕ) : + (r - 1) * b ≤ b.choose 2 + (r + 1).choose 2 := by + obtain _ | r := r + · simp + · rw [← Nat.cast_le (α := ℚ), Nat.cast_add, Nat.cast_choose_two, Nat.cast_choose_two] + push_cast + nlinarith [sq_nonneg ((r : ℚ) + 1 - b), (Nat.cast_nonneg r : (0 : ℚ) ≤ r), + (Nat.cast_nonneg b : (0 : ℚ) ≤ b)] + +private lemma sum_Ico_one_min_eq_choose {r : ℕ} (hr : 1 ≤ r) : + ∑ s ∈ Ico 1 r, min (r - 1) s = r.choose 2 := by + rw [sum_congr rfl (g := id) (by grind), ← Nat.sub_add_cancel hr, Ico_add_one_right_eq_Icc] + simpa using Nat.sum_Icc_choose (r - 1) 1 + +private lemma sum_Ico_min_eq_mul {b r : ℕ} : + ∑ s ∈ Ico r b, min (r - 1) s = (b - r) * (r - 1) := by + rw [sum_congr rfl (g := fun _ ↦ r - 1) (by grind)] + simp + +private lemma sum_Icc_min_sub {b r : ℕ} (hr : 1 ≤ r) (hrb : r ≤ b) : + ∑ t ∈ Icc 1 (b - 1), min (r - 1) (b - t) = r.choose 2 + (b - r) * (r - 1) := by + rw [← sum_Ico_one_min_eq_choose hr, ← sum_Ico_min_eq_mul, sum_Ico_consecutive _ hr hrb, + ← Ico_add_one_right_eq_Icc, Nat.sub_add_cancel (hr.trans hrb)] + convert sum_Ico_reflect (fun s ↦ min (r - 1) s) 1 (Nat.le_succ b) using 3 <;> grind + +/-- In a cancellative monoid, `|X + X| ≤ κ * |X|` for a nonempty `X` forces `1 ≤ κ`. -/ +private lemma one_le_of_card_add_le {G : Type*} [DecidableEq G] [AddCancelCommMonoid G] {κ : ℝ} + {X : Finset G} (hX : X.Nonempty) (hXX : (#(X + X) : ℝ) ≤ κ * #X) : 1 ≤ κ := by + have h : (#X : ℝ) ≤ κ * #X := (Nat.cast_le.2 (card_le_card_add_left hX)).trans hXX + nlinarith [(mod_cast hX.card_pos : (0 : ℝ) < #X)] + +/-- If `|X + X| ≤ κ * |X|` for a nonempty `X` and `f` is a Freiman isomorphism of order `2` from +`X` onto a subset of `ℝ^r` of affine dimension `r`, then `r ≤ 2 * κ - 1`. -/ +theorem le_two_mul_sub_one_of_isAddFreimanIso {G : Type*} [DecidableEq G] + [AddCancelCommMonoid G] {r : ℕ} {κ : ℝ} {X : Finset G} {f : G → Fin r → ℝ} + (hX : X.Nonempty) (hXX : (#(X + X) : ℝ) ≤ κ * #X) + (hf : IsAddFreimanIso 2 (X : Set G) (X.image f : Set (Fin r → ℝ)) f) + (hdim : (X.image f).affineDim = r) : (r : ℝ) ≤ 2 * κ - 1 := by + have hrX : r + 1 ≤ #X := by + grind [affineDim_add_one_le_card (hX.image f), card_image_of_injOn hf.bijOn.injOn] + have h : (2 * (#X + r * #X) : ℝ) ≤ 2 * #(X + X) + r * (r + 1) := + mod_cast two_mul_card_add_mul_card_le_of_isAddFreimanIso hX hf hdim + nlinarith [mul_nonneg (by positivity : (0 : ℝ) ≤ r + 1) + (sub_nonneg.2 (mod_cast hrX.trans' r.le_succ : (r : ℝ) ≤ #X)), + (mod_cast hX.card_pos : (0 : ℝ) < #X)] + +/-- The bound `r ≤ 2 * κ - 1` for a Freiman model, with the affine dimension of the model written +as the dimension of the span of its differences. -/ +theorem le_two_mul_sub_one_of_isAddFreimanIso_of_finrank_span_sub_eq {G : Type*} [DecidableEq G] + [AddCancelCommMonoid G] {r : ℕ} {κ : ℝ} {X : Finset G} {f : G → Fin r → ℝ} + (hX : X.Nonempty) (hXX : (#(X + X) : ℝ) ≤ κ * #X) + (hf : IsAddFreimanIso 2 (X : Set G) (X.image f : Set (Fin r → ℝ)) f) + (hdim : Module.finrank ℝ (Submodule.span ℝ (↑(X.image f) - ↑(X.image f) : Set (Fin r → ℝ))) = + r) : + (r : ℝ) ≤ 2 * κ - 1 := + le_two_mul_sub_one_of_isAddFreimanIso hX hXX hf + ((affineDim_eq_finrank_span_sub _).trans hdim) + +lemma sub_mul_sub_choose_le_sum_min (b r : ℕ) : + (r - 1) * b - (r + 1).choose 2 ≤ ∑ t ∈ Icc 1 (b - 1), min (r - 1) (b - t) := by + rw [Nat.sub_le_iff_le_add] + obtain hrb | hbr := le_total r b + · obtain rfl | hr := r.eq_zero_or_pos + · simp + · obtain ⟨c, rfl⟩ := Nat.exists_eq_add_of_le hrb + rw [sum_Icc_min_sub hr hrb, Nat.add_sub_cancel_left, mul_add] + linarith [sub_one_mul_le_choose_add_choose r r, mul_comm c (r - 1)] + · obtain rfl | hb := b.eq_zero_or_pos + · simp + · refine (sub_one_mul_le_choose_add_choose b r).trans ?_ + rw [← add_zero (b.choose 2), ← zero_mul (b - 1), ← Nat.sub_self b, + ← sum_Icc_min_sub hb le_rfl] + gcongr + +lemma sub_mul_sub_choose_le_sum_min_of_le {a b r d : ℕ} (hba : b ≤ a) (hrd : r ≤ d + 1) : + (r - 1) * b - (r + 1).choose 2 ≤ ∑ t ∈ Icc 1 (b - 1), min d (a - t) := by + refine (sub_mul_sub_choose_le_sum_min b r).trans ?_ + apply sum_le_sum + grind + +/-- Let `A` and `B` be finite with `B` nonempty and `|B| ≤ |A|`, and let `r ≥ 1` be the Freiman +dimension of `A ∪ B`. Then `|A| + ∑ t ∈ {1, …, |B| - 1}, min (r - 1) (|A| - t) ≤ |A + B|`. -/ +theorem card_add_sum_min_le_of_freimanDim_union {G : Type*} [DecidableEq G] [AddCommMonoid G] + {r : ℕ} {A B : Finset G} (hr : 1 ≤ r) (hB : B.Nonempty) (hBA : #B ≤ #A) + (hdim : freimanDim (A ∪ B) = r) : + #A + ∑ t ∈ Icc 1 (#B - 1), min (r - 1) (#A - t) ≤ #(A + B) := by + obtain ⟨f, hf, haff⟩ := exists_isAddFreimanIso_of_freimanDim_eq hdim (Nat.ne_of_gt hr) + exact card_add_sum_min_le_card_add_of_isAddFreimanIso hB hBA hf haff + +/-- Let `A` and `B` be finite with `B` nonempty and `|B| ≤ |A|`, and let `r ≥ 1` be the Freiman +dimension of `A ∪ B`. Then `|A| + (r - 1) * |B| - (r + 1).choose 2 ≤ |A + B|`. -/ +lemma card_add_mul_card_sub_choose_le_card_add_of_freimanDim_union + {G : Type*} [DecidableEq G] [AddCommMonoid G] {r : ℕ} {A B : Finset G} (hr : 1 ≤ r) + (hB : B.Nonempty) (hBA : #B ≤ #A) (hdim : freimanDim (A ∪ B) = r) : + #A + (r - 1) * #B - (r + 1).choose 2 ≤ #(A + B) := by + grind [card_add_sum_min_le_of_freimanDim_union hr hB hBA hdim, + sub_mul_sub_choose_le_sum_min_of_le (r := r) (d := r - 1) hBA (by grind)] + +/-- Freiman's lemma for `X + X` in terms of the Freiman dimension: if `X` is nonempty with Freiman +dimension `r ≥ 1`, then `(r + 1) * |X| - r * (r + 1) / 2 ≤ |X + X|`. -/ +lemma card_add_mul_card_sub_le_card_add_of_freimanDim {G : Type*} [DecidableEq G] + [AddCommMonoid G] {X : Finset G} (hX : X.Nonempty) (hr : freimanDim X ≠ 0) : + (freimanDim X + 1) * #X - freimanDim X * (freimanDim X + 1) / 2 ≤ #(X + X) := by + obtain ⟨f, hf, hdim⟩ := exists_isAddFreimanIso_of_freimanDim_eq rfl hr + grind [two_mul_card_add_mul_card_le_of_isAddFreimanIso hX hf hdim] + +/-- If `|X + X| ≤ κ * |X|` for a nonempty `X`, then `X` has Freiman dimension at most +`2 * κ - 1`. -/ +theorem freimanDim_le_two_mul_sub_one_of_card_add_le {G : Type*} [DecidableEq G] + [AddCancelCommMonoid G] {κ : ℝ} {X : Finset G} (hX : X.Nonempty) + (hXX : (#(X + X) : ℝ) ≤ κ * #X) : (freimanDim X : ℝ) ≤ 2 * κ - 1 := by + obtain hr | hr := (freimanDim X).eq_zero_or_pos + · rw [hr, Nat.cast_zero] + linarith [one_le_of_card_add_le hX hXX] + obtain ⟨f, hf, haff⟩ := exists_isAddFreimanIso_of_freimanDim_eq rfl hr.ne' + exact le_two_mul_sub_one_of_isAddFreimanIso hX hXX hf haff + +/-- If `|X + X| ≤ κ * |X|` for a nonempty `X` and `f` is a Freiman isomorphism of order `2` from +`X` onto a subset of `ℝ^r` of affine dimension `r`, then `r ≤ κ - 1 + κ * (2 * κ - 1) / |X|`. -/ +theorem le_sub_one_add_mul_div_card_of_isAddFreimanIso {G : Type*} [DecidableEq G] + [AddCancelCommMonoid G] {r : ℕ} {κ : ℝ} {X : Finset G} {f : G → Fin r → ℝ} + (hX : X.Nonempty) (hXX : (#(X + X) : ℝ) ≤ κ * #X) + (hf : IsAddFreimanIso 2 (X : Set G) (X.image f : Set (Fin r → ℝ)) f) + (hdim : (X.image f).affineDim = r) : r ≤ κ - 1 + κ * (2 * κ - 1) / #X := by + have h : (2 * (#X + r * #X) : ℝ) ≤ 2 * #(X + X) + r * (r + 1) := + mod_cast two_mul_card_add_mul_card_le_of_isAddFreimanIso hX hf hdim + have hr := le_two_mul_sub_one_of_isAddFreimanIso hX hXX hf hdim + rw [← sub_le_iff_le_add', le_div_iff₀ (mod_cast hX.card_pos)] + nlinarith [mul_nonneg (sub_nonneg.2 hr) (by linarith : (0 : ℝ) ≤ 2 * κ + r)] + +/-- The bound `r ≤ κ - 1 + κ * (2 * κ - 1) / |X|` for a Freiman model, with the affine dimension +of the model written as the dimension of the span of its differences. -/ +theorem le_sub_one_add_mul_div_card_of_isAddFreimanIso_of_finrank_span_sub_eq {G : Type*} + [DecidableEq G] [AddCancelCommMonoid G] {r : ℕ} {κ : ℝ} {X : Finset G} {f : G → Fin r → ℝ} + (hX : X.Nonempty) (hXX : (#(X + X) : ℝ) ≤ κ * #X) + (hf : IsAddFreimanIso 2 (X : Set G) (X.image f : Set (Fin r → ℝ)) f) + (hdim : Module.finrank ℝ (Submodule.span ℝ (↑(X.image f) - ↑(X.image f) : Set (Fin r → ℝ))) = + r) : + r ≤ κ - 1 + κ * (2 * κ - 1) / #X := + le_sub_one_add_mul_div_card_of_isAddFreimanIso hX hXX hf + ((affineDim_eq_finrank_span_sub _).trans hdim) + +/-- If `|X + X| ≤ κ * |X|` for a nonempty `X`, then `X` has Freiman dimension at most +`κ - 1 + κ * (2 * κ - 1) / |X|`. -/ +theorem freimanDim_le_sub_one_add_mul_div_card_of_card_add_le {G : Type*} [DecidableEq G] + [AddCancelCommMonoid G] {κ : ℝ} {X : Finset G} (hX : X.Nonempty) + (hXX : (#(X + X) : ℝ) ≤ κ * #X) : freimanDim X ≤ κ - 1 + κ * (2 * κ - 1) / #X := by + obtain hr | hr := (freimanDim X).eq_zero_or_pos + · rw [hr, Nat.cast_zero] + have hκ := one_le_of_card_add_le hX hXX + have : 0 ≤ κ * (2 * κ - 1) / #X := div_nonneg (by nlinarith) (Nat.cast_nonneg _) + linarith + obtain ⟨f, hf, haff⟩ := exists_isAddFreimanIso_of_freimanDim_eq rfl hr.ne' + exact le_sub_one_add_mul_div_card_of_isAddFreimanIso hX hXX hf haff + +end + +end SumOfSetsInSeveralDimensions diff --git a/LeanPool/SumOfSetsInSeveralDimensions/GeometricDeletion.lean b/LeanPool/SumOfSetsInSeveralDimensions/GeometricDeletion.lean new file mode 100644 index 0000000000..118f6065b7 --- /dev/null +++ b/LeanPool/SumOfSetsInSeveralDimensions/GeometricDeletion.lean @@ -0,0 +1,368 @@ +/- +Copyright (c) 2026 Gabriel Dahia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Dahia +-/ +module + +public import LeanPool.SumOfSetsInSeveralDimensions.AffineDim +public import Mathlib.Algebra.Group.Pointwise.Finset.Basic +public import Mathlib.Algebra.Order.Group.PiLex +import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional +import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas + +/-! +# Removing the origin from the summands + +This is Lemma 2.1 of Ruzsa's paper. Let `X, Y ⊆ ℝ^D` be finite sets with at least two points that +contain `0` and whose other elements are lexicographically positive. Write `X' = X \ {0}` and +`Y' = Y \ {0}`, let `d` be the affine dimension of `X + Y` and let `U` be the vector span of +`X' + Y'`. The lemma `geometric_deletion_cases` states that one of the following holds. + +* `X' + Y'` has dimension `d` and `|X + Y| ≥ |X' + Y'| + d + 1`. The points of `X + Y` outside + `X' + Y'` are `0` and the points of `C = (X' ∪ Y') \ (X' + Y')`. Every point of `X + Y` is a sum + of points of `C`, by induction along the lexicographic order, so `C` has at least `d` points. +* `X' + Y'` has dimension `d - 1` and `|X + Y| ≥ |Y| + |X' + Y'|`. Here `X'` has a point outside + `U`, and `Y` is disjoint from `X' + Y'`. +* `X' + Y` has dimension `d - 1` and `|X + Y| ≥ |Y| + |X' + Y|`. Here `X' + Y'` has dimension + `d - 2`, and `Y` is disjoint from `X' + Y`. +* `X + Y'` has dimension `d - 1` and `|X + Y| ≥ |X| + |X + Y'|`. Here `X' ⊆ U`, and `X` is disjoint + from `X + Y'`. +-/ + +public section + +namespace SumOfSetsInSeveralDimensions + +open Finset +open scoped Pointwise + +variable {D d : ℕ} {X Y : Finset (Fin D → ℝ)} {x₀ y₀ : Fin D → ℝ} + +private lemma affineDim_le_finrank_of_sub_mem {S : Finset (Fin D → ℝ)} + {U : Submodule ℝ (Fin D → ℝ)} {p : Fin D → ℝ} (hp : p ∈ S) (hS : ∀ x ∈ S, x - p ∈ U) : + S.affineDim ≤ Module.finrank ℝ U := by + rw [affineDim_eq_finrank_vectorSpan, vectorSpan_eq_span_vsub_set_right ℝ (mem_coe.2 hp)] + apply Submodule.finrank_mono + rw [Submodule.span_le] + rintro _ ⟨x, hx, rfl⟩ + exact hS x hx + +private lemma affineDim_add_le_finrank (h0X : 0 ∈ X) (h0Y : 0 ∈ Y) + {W : Submodule ℝ (Fin D → ℝ)} (hX : ∀ x ∈ X, x ∈ W) (hY : ∀ y ∈ Y, y ∈ W) : + (X + Y).affineDim ≤ Module.finrank ℝ W := by + refine affineDim_le_finrank_of_sub_mem (p := 0) (by simpa using add_mem_add h0X h0Y) ?_ + intro z hz + obtain ⟨x, hx, y, hy, rfl⟩ := mem_add.1 hz + simpa using W.add_mem (hX x hx) (hY y hy) + +private lemma finrank_sup_span_singleton_le (U : Submodule ℝ (Fin D → ℝ)) (v : Fin D → ℝ) : + Module.finrank ℝ ↥(U ⊔ ℝ ∙ v) ≤ Module.finrank ℝ U + 1 := by + apply (Submodule.finrank_add_le_finrank_add_finrank _ _).trans + gcongr + simpa using finrank_span_le_card ({v} : Set (Fin D → ℝ)) + +private lemma toLex_nonneg (hposY : ∀ y ∈ Y, y ≠ 0 → 0 < toLex y) {y : Fin D → ℝ} (hy : y ∈ Y) : + 0 ≤ toLex y := by + obtain rfl | hy0 := eq_or_ne y 0 + · simp + · exact (hposY y hy hy0).le + +private lemma add_ne_zero_of_ne_zero_left (hposX : ∀ x ∈ X, x ≠ 0 → 0 < toLex x) + (hposY : ∀ y ∈ Y, y ≠ 0 → 0 < toLex y) {x y : Fin D → ℝ} (hx : x ∈ X) (hx0 : x ≠ 0) + (hy : y ∈ Y) : x + y ≠ 0 := by + intro h + have h' := add_pos_of_pos_of_nonneg (hposX x hx hx0) (toLex_nonneg hposY hy) + rw [← toLex_add, h, toLex_zero] at h' + exact lt_irrefl 0 h' + +private lemma zero_notMem_erase_add_erase (hposX : ∀ x ∈ X, x ≠ 0 → 0 < toLex x) + (hposY : ∀ y ∈ Y, y ≠ 0 → 0 < toLex y) : (0 : Fin D → ℝ) ∉ X.erase 0 + Y.erase 0 := by + intro h + obtain ⟨x, hx, y, hy, hxy⟩ := mem_add.1 h + exact add_ne_zero_of_ne_zero_left hposX hposY (mem_of_mem_erase hx) (ne_of_mem_erase hx) + (mem_of_mem_erase hy) hxy + +/-! ### The case in which the dimension does not drop -/ + +private noncomputable def deletedComplement (X Y : Finset (Fin D → ℝ)) : Finset (Fin D → ℝ) := + (X.erase 0 ∪ Y.erase 0) \ (X.erase 0 + Y.erase 0) + +private lemma disjoint_deletedComplement : + Disjoint (X.erase 0 + Y.erase 0) (deletedComplement X Y) := + disjoint_sdiff + +private lemma mem_erase_union_erase {x y : Fin D → ℝ} (hx : x ∈ X) (hy : y ∈ Y) (h0 : x + y ≠ 0) + (h : x + y ∉ X.erase 0 + Y.erase 0) : x + y ∈ X.erase 0 ∪ Y.erase 0 := by + obtain rfl | hx0 := eq_or_ne x 0 + · simp_all + obtain rfl | hy0 := eq_or_ne y 0 + · simp_all + exact absurd (add_mem_add (mem_erase.2 ⟨hx0, hx⟩) (mem_erase.2 ⟨hy0, hy⟩)) h + +private lemma mem_span_deletedComplement (h0X : 0 ∈ X) (h0Y : 0 ∈ Y) + (hposX : ∀ x ∈ X, x ≠ 0 → 0 < toLex x) (hposY : ∀ y ∈ Y, y ≠ 0 → 0 < toLex y) + {z : Fin D → ℝ} (hz : z ∈ X + Y) : + z ∈ Submodule.span ℝ (deletedComplement X Y : Set (Fin D → ℝ)) := by + classical + by_contra hzC + obtain ⟨w, hw, hmin⟩ := exists_min_image + ((X + Y).filter (· ∉ Submodule.span ℝ (deletedComplement X Y : Set (Fin D → ℝ)))) toLex + ⟨z, mem_filter.2 ⟨hz, hzC⟩⟩ + obtain ⟨hwXY, hwC⟩ := mem_filter.1 hw + have hlt : ∀ v ∈ X + Y, toLex v < toLex w → + v ∈ Submodule.span ℝ (deletedComplement X Y : Set (Fin D → ℝ)) := by + intro v hv hvw + by_contra hvC + exact (hmin v (mem_filter.2 ⟨hv, hvC⟩)).not_gt hvw + apply hwC + by_cases hw' : w ∈ X.erase 0 + Y.erase 0 + · obtain ⟨x, hx, y, hy, rfl⟩ := mem_add.1 hw' + apply Submodule.add_mem + · apply hlt x (by simpa using add_mem_add (mem_of_mem_erase hx) h0Y) + rw [toLex_add] + exact lt_add_of_pos_right _ (hposY y (mem_of_mem_erase hy) (ne_of_mem_erase hy)) + · apply hlt y (by simpa using add_mem_add h0X (mem_of_mem_erase hy)) + rw [toLex_add] + exact lt_add_of_pos_left _ (hposX x (mem_of_mem_erase hx) (ne_of_mem_erase hx)) + · obtain rfl | hw0 := eq_or_ne w 0 + · exact Submodule.zero_mem _ + apply Submodule.subset_span + obtain ⟨x, hx, y, hy, rfl⟩ := mem_add.1 hwXY + exact mem_sdiff.2 ⟨mem_erase_union_erase hx hy hw0 hw', hw'⟩ + +private lemma insert_union_deletedComplement_subset (h0X : 0 ∈ X) (h0Y : 0 ∈ Y) : + insert 0 (X.erase 0 + Y.erase 0 ∪ deletedComplement X Y) ⊆ X + Y := by + intro z hz + obtain rfl | hz | hz := by simpa only [mem_insert, mem_union] using hz + · simpa using add_mem_add h0X h0Y + · exact add_subset_add (erase_subset _ _) (erase_subset _ _) hz + · obtain hz | hz := mem_union.1 (mem_sdiff.1 hz).1 + · simpa using add_mem_add (mem_of_mem_erase hz) h0Y + · simpa using add_mem_add h0X (mem_of_mem_erase hz) + +private lemma card_erase_add_erase_add_le (h0X : 0 ∈ X) (h0Y : 0 ∈ Y) + (hposX : ∀ x ∈ X, x ≠ 0 → 0 < toLex x) (hposY : ∀ y ∈ Y, y ≠ 0 → 0 < toLex y) : + #(X.erase 0 + Y.erase 0) + (X + Y).affineDim + 1 ≤ #(X + Y) := by + have hC : (X + Y).affineDim ≤ #(deletedComplement X Y) := by + refine (affineDim_le_finrank_of_sub_mem (p := 0) + (by simpa using add_mem_add h0X h0Y) ?_).trans (finrank_span_finset_le_card _) + intro z hz + simpa using mem_span_deletedComplement h0X h0Y hposX hposY hz + refine le_trans ?_ (card_le_card (insert_union_deletedComplement_subset h0X h0Y)) + rw [card_insert_of_notMem, card_union_of_disjoint disjoint_deletedComplement] + · grind + · rw [mem_union, not_or] + exact ⟨zero_notMem_erase_add_erase hposX hposY, fun h ↦ by simp [deletedComplement] at h⟩ + +/-! ### The cases in which the dimension drops -/ + +/-- The vector span `U` of `X' + Y'`. -/ +private noncomputable def deletedSpan (X Y : Finset (Fin D → ℝ)) : Submodule ℝ (Fin D → ℝ) := + vectorSpan ℝ (↑(X.erase 0 + Y.erase 0) : Set (Fin D → ℝ)) + +private lemma finrank_deletedSpan : + Module.finrank ℝ (deletedSpan X Y) = (X.erase 0 + Y.erase 0).affineDim := + (affineDim_eq_finrank_vectorSpan _).symm + +private lemma sub_mem_deletedSpan_left (hx₀ : x₀ ∈ X.erase 0) (hy₀ : y₀ ∈ Y.erase 0) + {x : Fin D → ℝ} (hx : x ∈ X.erase 0) : x - x₀ ∈ deletedSpan X Y := by + simpa [deletedSpan] using vsub_mem_vectorSpan ℝ (mem_coe.2 (add_mem_add hx hy₀)) + (mem_coe.2 (add_mem_add hx₀ hy₀)) + +private lemma sub_mem_deletedSpan_right (hx₀ : x₀ ∈ X.erase 0) (hy₀ : y₀ ∈ Y.erase 0) + {y : Fin D → ℝ} (hy : y ∈ Y.erase 0) : y - y₀ ∈ deletedSpan X Y := by + simpa [deletedSpan] using vsub_mem_vectorSpan ℝ (mem_coe.2 (add_mem_add hx₀ hy)) + (mem_coe.2 (add_mem_add hx₀ hy₀)) + +private lemma sub_add_mem_deletedSpan (hx₀ : x₀ ∈ X.erase 0) (hy₀ : y₀ ∈ Y.erase 0) + {z : Fin D → ℝ} (hz : z ∈ X.erase 0 + Y.erase 0) : z - (x₀ + y₀) ∈ deletedSpan X Y := + vsub_mem_vectorSpan ℝ (mem_coe.2 hz) (mem_coe.2 (add_mem_add hx₀ hy₀)) + +private lemma mem_of_le_left (hx₀ : x₀ ∈ X.erase 0) (hy₀ : y₀ ∈ Y.erase 0) + {W : Submodule ℝ (Fin D → ℝ)} (hUW : deletedSpan X Y ≤ W) (hx₀W : x₀ ∈ W) {x : Fin D → ℝ} + (hx : x ∈ X) : x ∈ W := by + obtain rfl | hx0 := eq_or_ne x 0 + · exact W.zero_mem + rw [← sub_add_cancel x x₀] + exact W.add_mem (hUW (sub_mem_deletedSpan_left hx₀ hy₀ (mem_erase.2 ⟨hx0, hx⟩))) hx₀W + +private lemma mem_of_le_right (hx₀ : x₀ ∈ X.erase 0) (hy₀ : y₀ ∈ Y.erase 0) + {W : Submodule ℝ (Fin D → ℝ)} (hUW : deletedSpan X Y ≤ W) (hy₀W : y₀ ∈ W) {y : Fin D → ℝ} + (hy : y ∈ Y) : y ∈ W := by + obtain rfl | hy0 := eq_or_ne y 0 + · exact W.zero_mem + rw [← sub_add_cancel y y₀] + exact W.add_mem (hUW (sub_mem_deletedSpan_right hx₀ hy₀ (mem_erase.2 ⟨hy0, hy⟩))) hy₀W + +private lemma affineDim_add_le_add_two (h0X : 0 ∈ X) (h0Y : 0 ∈ Y) + (hx₀ : x₀ ∈ X.erase 0) (hy₀ : y₀ ∈ Y.erase 0) : + (X + Y).affineDim ≤ (X.erase 0 + Y.erase 0).affineDim + 2 := by + refine (affineDim_add_le_finrank h0X h0Y + (W := deletedSpan X Y ⊔ ℝ ∙ x₀ ⊔ ℝ ∙ y₀) ?_ ?_).trans ?_ + · intro x hx + exact mem_of_le_left hx₀ hy₀ (le_sup_left.trans le_sup_left) + (Submodule.mem_sup_left (Submodule.mem_sup_right (Submodule.mem_span_singleton_self x₀))) hx + · intro y hy + exact mem_of_le_right hx₀ hy₀ (le_sup_left.trans le_sup_left) + (Submodule.mem_sup_right (Submodule.mem_span_singleton_self y₀)) hy + · grind [finrank_sup_span_singleton_le (deletedSpan X Y ⊔ ℝ ∙ x₀) y₀, + finrank_sup_span_singleton_le (deletedSpan X Y) x₀, finrank_deletedSpan (X := X) (Y := Y)] + +/-- The case in which `x₀ ∈ U`: then `X ⊆ U`, and `X + Y'` lies in the translate `U + y₀`, which +does not meet `U`. -/ +private lemma deletion_right_of_mem (h0X : 0 ∈ X) (h0Y : 0 ∈ Y) (hx₀ : x₀ ∈ X.erase 0) + (hy₀ : y₀ ∈ Y.erase 0) (hdim : (X + Y).affineDim = d) + (hlt : (X.erase 0 + Y.erase 0).affineDim < d) (hxU : x₀ ∈ deletedSpan X Y) : + (X + Y.erase 0).affineDim = d - 1 ∧ #X + #(X + Y.erase 0) ≤ #(X + Y) := by + have hX : ∀ x ∈ X, x ∈ deletedSpan X Y := fun x hx ↦ mem_of_le_left hx₀ hy₀ le_rfl hxU hx + have hyU : y₀ ∉ deletedSpan X Y := by + intro hyU + grind [affineDim_add_le_finrank h0X h0Y hX + (fun y hy ↦ mem_of_le_right hx₀ hy₀ le_rfl hyU hy), finrank_deletedSpan (X := X) (Y := Y)] + have hd : d ≤ (X.erase 0 + Y.erase 0).affineDim + 1 := by + grind [affineDim_add_le_finrank h0X h0Y (W := deletedSpan X Y ⊔ ℝ ∙ y₀) + (fun x hx ↦ Submodule.mem_sup_left (hX x hx)) + (fun y hy ↦ mem_of_le_right hx₀ hy₀ le_sup_left + (Submodule.mem_sup_right (Submodule.mem_span_singleton_self y₀)) hy), + finrank_sup_span_singleton_le (deletedSpan X Y) y₀, finrank_deletedSpan (X := X) (Y := Y)] + refine ⟨le_antisymm ?_ ?_, ?_⟩ + · refine (affineDim_le_finrank_of_sub_mem (U := deletedSpan X Y) + (by simpa using add_mem_add h0X hy₀) ?_).trans ?_ + · intro z hz + obtain ⟨x, hx, y, hy, rfl⟩ := mem_add.1 hz + rw [add_sub_assoc] + exact Submodule.add_mem _ (hX x hx) (sub_mem_deletedSpan_right hx₀ hy₀ hy) + · grind [finrank_deletedSpan (X := X) (Y := Y)] + · grind [affineDim_mono (add_subset_add_right (t := Y.erase 0) (erase_subset 0 X))] + · rw [← card_union_of_disjoint] + · refine card_le_card (union_subset ?_ (add_subset_add_left (erase_subset _ _))) + intro x hx + simpa using add_mem_add hx h0Y + · rw [disjoint_left] + intro z hz hzY + obtain ⟨x, hx, y, hy, rfl⟩ := mem_add.1 hzY + apply hyU + rw [(by abel : y₀ = x + y - x - (y - y₀))] + exact Submodule.sub_mem _ (Submodule.sub_mem _ (hX _ hz) (hX x hx)) + (sub_mem_deletedSpan_right hx₀ hy₀ hy) + +/-- The case in which `x₀ ∉ U` and `U` has dimension `d - 1`: `Y` does not meet `X' + Y'`. -/ +private lemma card_add_card_erase_add_erase_le (hposX : ∀ x ∈ X, x ≠ 0 → 0 < toLex x) + (hposY : ∀ y ∈ Y, y ≠ 0 → 0 < toLex y) (h0X : 0 ∈ X) (hx₀ : x₀ ∈ X.erase 0) + (hy₀ : y₀ ∈ Y.erase 0) (hxU : x₀ ∉ deletedSpan X Y) : + #Y + #(X.erase 0 + Y.erase 0) ≤ #(X + Y) := by + rw [← card_union_of_disjoint] + · refine card_le_card (union_subset ?_ (add_subset_add (erase_subset _ _) (erase_subset _ _))) + intro y hy + simpa using add_mem_add h0X hy + · rw [disjoint_left] + intro z hzY hz + have hz0 : z ≠ 0 := fun h ↦ zero_notMem_erase_add_erase hposX hposY (h ▸ hz) + apply hxU + rw [(by abel : x₀ = z - y₀ - (z - (x₀ + y₀)))] + exact Submodule.sub_mem _ (sub_mem_deletedSpan_right hx₀ hy₀ (mem_erase.2 ⟨hz0, hzY⟩)) + (sub_add_mem_deletedSpan hx₀ hy₀ hz) + +private lemma notMem_sup_of_affineDim_eq (h0X : 0 ∈ X) (h0Y : 0 ∈ Y) + (hx₀ : x₀ ∈ X.erase 0) (hy₀ : y₀ ∈ Y.erase 0) (hdim : (X + Y).affineDim = d) + (hdel : (X.erase 0 + Y.erase 0).affineDim + 2 = d) : + y₀ ∉ deletedSpan X Y ⊔ ℝ ∙ x₀ := by + intro hyW + grind [affineDim_add_le_finrank h0X h0Y + (fun x hx ↦ mem_of_le_left hx₀ hy₀ le_sup_left + (Submodule.mem_sup_right (Submodule.mem_span_singleton_self x₀)) hx) + (fun y hy ↦ mem_of_le_right hx₀ hy₀ le_sup_left hyW hy), + finrank_sup_span_singleton_le (deletedSpan X Y) x₀, finrank_deletedSpan (X := X) (Y := Y)] + +private lemma affineDim_erase_add_eq (h0Y : 0 ∈ Y) (hx₀ : x₀ ∈ X.erase 0) + (hy₀ : y₀ ∈ Y.erase 0) (hyW : y₀ ∉ deletedSpan X Y ⊔ ℝ ∙ x₀) : + (X.erase 0 + Y).affineDim = (X.erase 0 + Y.erase 0).affineDim + 1 := by + rw [← finrank_deletedSpan, ← Submodule.finrank_sup_span_singleton + (fun h ↦ hyW (Submodule.mem_sup_left h))] + apply le_antisymm + · refine affineDim_le_finrank_of_sub_mem (by simpa using add_mem_add hx₀ h0Y) ?_ + intro z hz + obtain ⟨x, hx, y, hy, rfl⟩ := mem_add.1 hz + rw [add_sub_right_comm] + exact Submodule.add_mem _ (Submodule.mem_sup_left (sub_mem_deletedSpan_left hx₀ hy₀ hx)) + (mem_of_le_right hx₀ hy₀ le_sup_left + (Submodule.mem_sup_right (Submodule.mem_span_singleton_self y₀)) hy) + · rw [affineDim_eq_finrank_vectorSpan] + apply Submodule.finrank_mono + refine sup_le (vectorSpan_mono ℝ (coe_subset.2 (add_subset_add_left (erase_subset _ _)))) ?_ + rw [Submodule.span_singleton_le_iff_mem] + simpa using vsub_mem_vectorSpan ℝ (mem_coe.2 (add_mem_add hx₀ (mem_of_mem_erase hy₀))) + (mem_coe.2 (add_mem_add hx₀ h0Y)) + +/-- The case in which `x₀ ∉ U` and `U` has dimension `d - 2`: `Y` does not meet `X' + Y`. -/ +private lemma card_add_card_erase_add_le (hposX : ∀ x ∈ X, x ≠ 0 → 0 < toLex x) + (hposY : ∀ y ∈ Y, y ≠ 0 → 0 < toLex y) (h0X : 0 ∈ X) (hx₀ : x₀ ∈ X.erase 0) + (hy₀ : y₀ ∈ Y.erase 0) (hxU : x₀ ∉ deletedSpan X Y) (hyW : y₀ ∉ deletedSpan X Y ⊔ ℝ ∙ x₀) : + #Y + #(X.erase 0 + Y) ≤ #(X + Y) := by + rw [← card_union_of_disjoint] + · refine card_le_card (union_subset ?_ (add_subset_add_right (erase_subset _ _))) + intro y hy + simpa using add_mem_add h0X hy + · rw [disjoint_left] + intro z hzY hz + obtain ⟨x, hx, y, hy, rfl⟩ := mem_add.1 hz + have hz0 := add_ne_zero_of_ne_zero_left hposX hposY (mem_of_mem_erase hx) (ne_of_mem_erase hx) + hy + obtain rfl | hy0 := eq_or_ne y 0 + · apply hyW + rw [add_zero] at hzY hz0 + rw [(by abel : y₀ = x - x₀ - (x - y₀) + x₀)] + exact Submodule.add_mem_sup (Submodule.sub_mem _ (sub_mem_deletedSpan_left hx₀ hy₀ hx) + (sub_mem_deletedSpan_right hx₀ hy₀ (mem_erase.2 ⟨hz0, hzY⟩))) + (Submodule.mem_span_singleton_self x₀) + · apply hxU + rw [(by abel : x₀ = x + y - y₀ - (y - y₀) - (x - x₀))] + exact Submodule.sub_mem _ (Submodule.sub_mem _ + (sub_mem_deletedSpan_right hx₀ hy₀ (mem_erase.2 ⟨hz0, hzY⟩)) + (sub_mem_deletedSpan_right hx₀ hy₀ (mem_erase.2 ⟨hy0, hy⟩))) + (sub_mem_deletedSpan_left hx₀ hy₀ hx) + +/-- **Lemma 2.1 of Ruzsa.** Let `X` and `Y` contain `0`, have at least two points each, and have +all other elements lexicographically positive, and let `X + Y` have affine dimension `d`. Then +removing `0` from `X`, from `Y` or from both gives a sumset of dimension `d` with at least `d + 1` +fewer points, or a sumset of dimension `d - 1` with at least `|Y|` or `|X|` fewer points, as +listed in the statement. -/ +lemma geometric_deletion_cases (h0X : 0 ∈ X) (h0Y : 0 ∈ Y) + (hposX : ∀ x ∈ X, x ≠ 0 → 0 < toLex x) (hposY : ∀ y ∈ Y, y ≠ 0 → 0 < toLex y) + (hXcard : 2 ≤ #X) (hYcard : 2 ≤ #Y) (hdim : (X + Y).affineDim = d) : + ((X.erase 0 + Y.erase 0).affineDim = d ∧ + #(X.erase 0 + Y.erase 0) + d + 1 ≤ #(X + Y)) ∨ + ((X.erase 0 + Y.erase 0).affineDim = d - 1 ∧ + #Y + #(X.erase 0 + Y.erase 0) ≤ #(X + Y)) ∨ + ((X.erase 0 + Y).affineDim = d - 1 ∧ #Y + #(X.erase 0 + Y) ≤ #(X + Y)) ∨ + ((X + Y.erase 0).affineDim = d - 1 ∧ #X + #(X + Y.erase 0) ≤ #(X + Y)) := by + obtain hdel | hdel := eq_or_ne ((X.erase 0 + Y.erase 0).affineDim) d + · left + refine ⟨hdel, ?_⟩ + grind [card_erase_add_erase_add_le h0X h0Y hposX hposY] + right + have hlt : (X.erase 0 + Y.erase 0).affineDim < d := by + grind [affineDim_mono (add_subset_add (erase_subset 0 X) (erase_subset 0 Y))] + obtain ⟨x₀, hx₀⟩ : (X.erase 0).Nonempty := by + rw [← card_pos, card_erase_of_mem h0X] + grind + obtain ⟨y₀, hy₀⟩ : (Y.erase 0).Nonempty := by + rw [← card_pos, card_erase_of_mem h0Y] + grind + by_cases hxU : x₀ ∈ deletedSpan X Y + · right + right + exact deletion_right_of_mem h0X h0Y hx₀ hy₀ hdim hlt hxU + obtain hcodim | hcodim : (X.erase 0 + Y.erase 0).affineDim + 1 = d ∨ + (X.erase 0 + Y.erase 0).affineDim + 2 = d := by + grind [affineDim_add_le_add_two h0X h0Y hx₀ hy₀] + · left + exact ⟨by grind, card_add_card_erase_add_erase_le hposX hposY h0X hx₀ hy₀ hxU⟩ + · right + left + have hyW := notMem_sup_of_affineDim_eq h0X h0Y hx₀ hy₀ hdim hcodim + exact ⟨by grind [affineDim_erase_add_eq h0Y hx₀ hy₀ hyW], + card_add_card_erase_add_le hposX hposY h0X hx₀ hy₀ hxU hyW⟩ + +end SumOfSetsInSeveralDimensions diff --git a/LeanPool/SumOfSetsInSeveralDimensions/Imports.lean b/LeanPool/SumOfSetsInSeveralDimensions/Imports.lean new file mode 100644 index 0000000000..168e8a973a --- /dev/null +++ b/LeanPool/SumOfSetsInSeveralDimensions/Imports.lean @@ -0,0 +1,21 @@ +/- +Copyright (c) 2026 Lean Pool contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lean Pool contributors +-/ +module -- shake: keep-all --deprecated_module: ignore + +-- Generated project imports; run `lake exe mk_all`. +public import LeanPool.SumOfSetsInSeveralDimensions +public import LeanPool.SumOfSetsInSeveralDimensions.AffineDim +public import LeanPool.SumOfSetsInSeveralDimensions.AffineDimSumset +public import LeanPool.SumOfSetsInSeveralDimensions.ClosedForm +public import LeanPool.SumOfSetsInSeveralDimensions.Construction +public import LeanPool.SumOfSetsInSeveralDimensions.FreimanDimension +public import LeanPool.SumOfSetsInSeveralDimensions.FreimanDimensionSumsetBounds +public import LeanPool.SumOfSetsInSeveralDimensions.GeometricDeletion +public import LeanPool.SumOfSetsInSeveralDimensions.LowerBound +public import LeanPool.SumOfSetsInSeveralDimensions.LowerBoundFunction +public import LeanPool.SumOfSetsInSeveralDimensions.LowerBoundValues +public import LeanPool.SumOfSetsInSeveralDimensions.MinCardAdd +public import LeanPool.SumOfSetsInSeveralDimensions.Normalize diff --git a/LeanPool/SumOfSetsInSeveralDimensions/LowerBound.lean b/LeanPool/SumOfSetsInSeveralDimensions/LowerBound.lean new file mode 100644 index 0000000000..48f4d4382b --- /dev/null +++ b/LeanPool/SumOfSetsInSeveralDimensions/LowerBound.lean @@ -0,0 +1,113 @@ +/- +Copyright (c) 2026 Gabriel Dahia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Dahia +-/ +module + +public import LeanPool.SumOfSetsInSeveralDimensions.AffineDim +public import Mathlib.Algebra.BigOperators.Group.Finset.Basic +public import Mathlib.Algebra.Group.Pointwise.Finset.Basic +public import Mathlib.Order.Interval.Finset.Nat +import LeanPool.SumOfSetsInSeveralDimensions.GeometricDeletion +import LeanPool.SumOfSetsInSeveralDimensions.LowerBoundFunction +import LeanPool.SumOfSetsInSeveralDimensions.Normalize +import Mathlib.Algebra.Order.BigOperators.Group.Finset + +/-! +# Sum of sets in several dimensions + +Theorem 1 of Ruzsa, *Sum of sets in several dimensions*, Combinatorica 14 (1994): if +`A, B ⊆ ℝ^D` are finite sets with `B` nonempty and `|B| ≤ |A|`, and `A + B` has affine dimension +`d`, then `|A + B| ≥ |A| + ∑ t ∈ {1, …, |B| - 1}, min d (|A| - t)`. + +The proof is by induction on `|A| + |B|`. Both sets are translated so that their +lexicographically least element is `0`. If `|B| ≥ 2`, the lemma `geometric_deletion_cases` removes +`0` from one or both of the sets, and the inequalities of `LowerBoundFunction.lean` compare the +bound for the smaller sets with the bound for `A` and `B`. + +## Main statements + +* `card_add_sum_min_le_card_add`: Ruzsa's theorem. +* `card_add_sum_min_le_card_add_of_le`: the same bound for every `d` at most the affine dimension + of `A + B`. +* `card_add_sum_min_le_card_add_of_finrank_span_sub_eq`: Ruzsa's theorem, with the affine + dimension written as the dimension of the span of `(A + B) - (A + B)`. +-/ + +public section + +namespace SumOfSetsInSeveralDimensions + +open Finset +open scoped Pointwise + +/-- The inductive step for sets `X` and `Y` that contain `0` and whose other elements are +lexicographically positive, given the bound for all pairs of sets with fewer points. -/ +private lemma sumsetCardLowerBound_le_card_add_of_zero_mem {D d : ℕ} {X Y : Finset (Fin D → ℝ)} + (ih : ∀ {e m n : ℕ} {X' Y' : Finset (Fin D → ℝ)}, #X' = m → #Y' = n → + m + n < #X + #Y → 1 ≤ m → m ≤ n → (X' + Y').affineDim = e → + sumsetCardLowerBound e m n ≤ #(X' + Y')) + (h0X : 0 ∈ X) (h0Y : 0 ∈ Y) (hposX : ∀ x ∈ X, x ≠ 0 → 0 < toLex x) + (hposY : ∀ y ∈ Y, y ≠ 0 → 0 < toLex y) (hX : 2 ≤ #X) (hXY : #X ≤ #Y) + (hdim : (X + Y).affineDim = d) : + sumsetCardLowerBound d #X #Y ≤ #(X + Y) := by + obtain ⟨hd, hcard⟩ | ⟨hd, hcard⟩ | ⟨hd, hcard⟩ | ⟨hd, hcard⟩ := + geometric_deletion_cases h0X h0Y hposX hposY hX (hX.trans hXY) hdim + · refine sumsetCardLowerBound_of_full_case hX ?_ hcard + exact ih (card_erase_of_mem h0X) (card_erase_of_mem h0Y) (by grind) (by grind) (by grind) hd + · refine sumsetCardLowerBound_of_large_case hX hXY ?_ hcard + exact ih (card_erase_of_mem h0X) (card_erase_of_mem h0Y) (by grind) (by grind) (by grind) hd + · refine sumsetCardLowerBound_of_small_case hX hXY ?_ hcard + exact ih (card_erase_of_mem h0X) rfl (by grind) (by grind) (by grind) hd + obtain hXY | hXY := hXY.eq_or_lt + · rw [add_comm X (Y.erase 0)] at hd hcard + rw [← hXY] + refine sumsetCardLowerBound_of_equal_right_case hX ?_ hcard + exact ih (by grind [card_erase_of_mem h0Y]) rfl (by grind) (by grind) (by grind) hd + · refine sumsetCardLowerBound_of_strict_right_case (by grind) hXY ?_ hcard + exact ih rfl (card_erase_of_mem h0Y) (by grind) (by grind) (by grind) hd + +private lemma sumsetCardLowerBound_le_card_add {D d : ℕ} {A B : Finset (Fin D → ℝ)} + (hB : B.Nonempty) (hBA : #B ≤ #A) (hdim : (A + B).affineDim = d) : + sumsetCardLowerBound d #B #A ≤ #(A + B) := by + generalize hn : #A + #B = n + induction n using Nat.strong_induction_on generalizing d A B with + | _ n ih => + obtain hB1 | hB2 : #B = 1 ∨ 2 ≤ #B := by grind [hB.card_pos] + · rw [sumsetCardLowerBound_eq, hB1] + simpa using card_le_card_add_right hB + have hA : A.Nonempty := card_pos.1 (by grind) + rw [← normalize_add_card hA hB, ← normalize_card hB, ← normalize_card hA, add_comm] + refine sumsetCardLowerBound_le_card_add_of_zero_mem ?_ (zero_mem_normalize hB) + (zero_mem_normalize hA) (fun x hx hx0 ↦ normalize_pos_of_ne_zero hB hx hx0) + (fun y hy hy0 ↦ normalize_pos_of_ne_zero hA hy hy0) (by simpa [normalize_card] using hB2) + (by simpa [normalize_card] using hBA) (by rwa [add_comm, normalize_add_dim]) + rintro e m k X Y rfl rfl hlt hm hmk hdim' + rw [add_comm X] at hdim' ⊢ + exact ih _ (by grind [normalize_card hA, normalize_card hB]) (card_pos.1 hm) hmk hdim' rfl + +/-- **Ruzsa's theorem.** If `A, B ⊆ ℝ^D` are finite, `B` is nonempty, `|B| ≤ |A|` and `A + B` has +affine dimension `d`, then `|A| + ∑ t ∈ {1, …, |B| - 1}, min d (|A| - t) ≤ |A + B|`. -/ +theorem card_add_sum_min_le_card_add {D d : ℕ} {A B : Finset (Fin D → ℝ)} + (hB : B.Nonempty) (hBA : #B ≤ #A) (hdim : (A + B).affineDim = d) : + #A + ∑ t ∈ Icc 1 (#B - 1), min d (#A - t) ≤ #(A + B) := by + rw [← sumsetCardLowerBound_eq] + exact sumsetCardLowerBound_le_card_add hB hBA hdim + +/-- Ruzsa's theorem for every `d` at most the affine dimension of `A + B`. -/ +lemma card_add_sum_min_le_card_add_of_le {D d : ℕ} {A B : Finset (Fin D → ℝ)} + (hB : B.Nonempty) (hBA : #B ≤ #A) (hd : d ≤ (A + B).affineDim) : + #A + ∑ t ∈ Icc 1 (#B - 1), min d (#A - t) ≤ #(A + B) := by + refine le_trans ?_ (card_add_sum_min_le_card_add hB hBA rfl) + gcongr + +/-- Ruzsa's theorem, with the affine dimension of `A + B` written as the dimension of the span of +`(A + B) - (A + B)`. -/ +theorem card_add_sum_min_le_card_add_of_finrank_span_sub_eq {D d : ℕ} + {A B : Finset (Fin D → ℝ)} (hB : B.Nonempty) (hBA : #B ≤ #A) + (hdim : Module.finrank ℝ (Submodule.span ℝ (↑(A + B) - ↑(A + B) : Set (Fin D → ℝ))) = d) : + #A + ∑ t ∈ Icc 1 (#B - 1), min d (#A - t) ≤ #(A + B) := + card_add_sum_min_le_card_add hB hBA ((affineDim_eq_finrank_span_sub _).trans hdim) + +end SumOfSetsInSeveralDimensions diff --git a/LeanPool/SumOfSetsInSeveralDimensions/LowerBoundFunction.lean b/LeanPool/SumOfSetsInSeveralDimensions/LowerBoundFunction.lean new file mode 100644 index 0000000000..45ba460f48 --- /dev/null +++ b/LeanPool/SumOfSetsInSeveralDimensions/LowerBoundFunction.lean @@ -0,0 +1,111 @@ +/- +Copyright (c) 2026 Gabriel Dahia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Dahia +-/ +module + +public import Mathlib.Algebra.BigOperators.Group.Finset.Basic +public import Mathlib.Order.Interval.Finset.Nat +import Mathlib.Algebra.BigOperators.Intervals +import Mathlib.Algebra.Group.Action.Defs +import Mathlib.Algebra.Order.BigOperators.Group.Finset +import Mathlib.Algebra.Order.Interval.Finset.SuccPred + +/-! +# The lower bound as a function of the dimension and the cardinalities + +The lower bound in Ruzsa's theorem for sets `A` and `B` with `|A| = n ≥ |B| = m` and `A + B` of +affine dimension `d` is `sumsetCardLowerBound d m n = n + ∑ t ∈ {1, …, m - 1}, min d (n - t)`, the +function `G_d(m, n)` of the paper. The induction in the proof removes one point from `A`, from +`B`, or from both, and the dimension stays the same or drops by one. This file proves the +inequality between the values of the bound that each of these cases needs. +-/ + +@[expose] public section + +namespace SumOfSetsInSeveralDimensions + +open Finset + +/-- The lower bound `G_d(m, n)` of Ruzsa's theorem for the size of a sumset of affine dimension `d` +of sets of sizes `m ≤ n`. -/ +def sumsetCardLowerBound (d m n : ℕ) : ℕ := + n + ∑ t ∈ Icc 1 (m - 1), min d (n - t) + +/-- The definition of `sumsetCardLowerBound`. -/ +lemma sumsetCardLowerBound_eq (d m n : ℕ) : + sumsetCardLowerBound d m n = n + ∑ t ∈ Icc 1 (m - 1), min d (n - t) := by + rfl + +private lemma sum_Icc_one_add_one (f : ℕ → ℕ) (k : ℕ) : + ∑ t ∈ Icc 1 (k + 1), f t = f 1 + ∑ t ∈ Icc 1 k, f (t + 1) := by + rw [← add_sum_Ioc_eq_sum_Icc (by grind), ← Icc_add_one_left_eq_Ioc, ← map_add_right_Icc, + sum_map] + rfl + +private lemma sum_min_le_sum_min_sub_one_add (d n k : ℕ) : + ∑ t ∈ Icc 1 k, min d (n - t) ≤ ∑ t ∈ Icc 1 k, min (d - 1) (n - 1 - t) + k := by + refine (sum_le_sum (g := fun t ↦ min (d - 1) (n - 1 - t) + 1) ?_).trans ?_ + · grind + · rw [sum_add_distrib, sum_const, Nat.card_Icc, smul_eq_mul, mul_one, Nat.add_sub_cancel] + +/-- `G_d(m, n) = G_d(m - 1, n - 1) + min (d + 1) n` for `m ≥ 2`. -/ +lemma sumsetCardLowerBound_eq_add_min {d m n : ℕ} (hm : 2 ≤ m) : + sumsetCardLowerBound d m n = sumsetCardLowerBound d (m - 1) (n - 1) + min (d + 1) n := by + obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le' hm + rw [sumsetCardLowerBound_eq, sumsetCardLowerBound_eq, (by grind : k + 2 - 1 = k + 1), + (by grind : k + 1 - 1 = k), sum_Icc_one_add_one] + simp only [Nat.sub_add_eq, Nat.sub_right_comm _ _ 1] + grind + +private lemma sumsetCardLowerBound_le_large_deletion {d m n : ℕ} (hm : 2 ≤ m) (hmn : m ≤ n) : + sumsetCardLowerBound d m n ≤ n + sumsetCardLowerBound (d - 1) (m - 1) (n - 1) := by + obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le' hm + rw [sumsetCardLowerBound_eq, sumsetCardLowerBound_eq, (by grind : k + 2 - 1 = k + 1), + (by grind : k + 1 - 1 = k), sum_Icc_succ_top (by grind)] + grind [sum_min_le_sum_min_sub_one_add d n k] + +private lemma sumsetCardLowerBound_mono_right (d m : ℕ) : Monotone (sumsetCardLowerBound d m) := by + intro a b hab + rw [sumsetCardLowerBound_eq, sumsetCardLowerBound_eq] + gcongr + +/-- The case in which one point is removed from each set and the dimension does not change: the +sumset loses at least `d + 1` points. -/ +lemma sumsetCardLowerBound_of_full_case {d m n p s : ℕ} (hm : 2 ≤ m) + (hrec : sumsetCardLowerBound d (m - 1) (n - 1) ≤ p) (hcard : p + d + 1 ≤ s) : + sumsetCardLowerBound d m n ≤ s := by + grind [sumsetCardLowerBound_eq_add_min (d := d) (n := n) hm] + +/-- The case in which one point is removed from each set and the dimension drops by one: the +sumset loses at least `n` points. -/ +lemma sumsetCardLowerBound_of_large_case {d m n p s : ℕ} (hm : 2 ≤ m) (hmn : m ≤ n) + (hrec : sumsetCardLowerBound (d - 1) (m - 1) (n - 1) ≤ p) (hcard : n + p ≤ s) : + sumsetCardLowerBound d m n ≤ s := by + grind [sumsetCardLowerBound_le_large_deletion (d := d) hm hmn] + +/-- The case in which one point is removed from the smaller set and the dimension drops by one: +the sumset loses at least `n` points. -/ +lemma sumsetCardLowerBound_of_small_case {d m n p s : ℕ} (hm : 2 ≤ m) (hmn : m ≤ n) + (hrec : sumsetCardLowerBound (d - 1) (m - 1) n ≤ p) (hcard : n + p ≤ s) : + sumsetCardLowerBound d m n ≤ s := by + grind [sumsetCardLowerBound_le_large_deletion (d := d) hm hmn, + sumsetCardLowerBound_mono_right (d - 1) (m - 1) (n.sub_le 1)] + +/-- The case in which the sets have the same size `m`, one point is removed from one of them and +the dimension drops by one: the sumset loses at least `m` points. -/ +lemma sumsetCardLowerBound_of_equal_right_case {d m p s : ℕ} (hm : 2 ≤ m) + (hrec : sumsetCardLowerBound (d - 1) (m - 1) m ≤ p) (hcard : m + p ≤ s) : + sumsetCardLowerBound d m m ≤ s := + sumsetCardLowerBound_of_small_case hm le_rfl hrec hcard + +/-- The case in which one point is removed from the strictly larger set and the dimension drops +by one: the sumset loses at least `m` points. -/ +lemma sumsetCardLowerBound_of_strict_right_case {d m n p s : ℕ} (hm : 1 ≤ m) (hmn : m < n) + (hrec : sumsetCardLowerBound (d - 1) m (n - 1) ≤ p) (hcard : m + p ≤ s) : + sumsetCardLowerBound d m n ≤ s := by + rw [sumsetCardLowerBound_eq] at hrec ⊢ + grind [sum_min_le_sum_min_sub_one_add d n (m - 1)] + +end SumOfSetsInSeveralDimensions diff --git a/LeanPool/SumOfSetsInSeveralDimensions/LowerBoundValues.lean b/LeanPool/SumOfSetsInSeveralDimensions/LowerBoundValues.lean new file mode 100644 index 0000000000..d2f2e0506b --- /dev/null +++ b/LeanPool/SumOfSetsInSeveralDimensions/LowerBoundValues.lean @@ -0,0 +1,98 @@ +/- +Copyright (c) 2026 Gabriel Dahia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Dahia +-/ +module + +public import LeanPool.SumOfSetsInSeveralDimensions.LowerBoundFunction +import Mathlib.Algebra.BigOperators.Intervals +import Mathlib.Algebra.Order.BigOperators.Group.Finset +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Ring + +/-! +# The values of the lower bound + +The formulas (1.5), (1.6) and (1.7) of Ruzsa's paper for `G_d(m, n) = sumsetCardLowerBound d m n` +when `m ≤ n`. Write `t = n - m`. + +* `sumsetCardLowerBound_of_add_le`: if `t ≥ d - 1`, then `G_d(m, n) = n + d * (m - 1)`. The paper + states this for `t ≥ d`. +* `two_mul_sumsetCardLowerBound_add_add`, `two_mul_sumsetCardLowerBound_add`: if `t < d < n`, + then `2 * G_d(m, n) = 2 * n * (d + 1) - d * (d + 1) - t * (t + 1)` and + `2 * G_d(m, n) = 2 * (n + d * (m - 1)) - (d - t) * (d - t - 1)`. +* `two_mul_sumsetCardLowerBound_of_le`: if `1 ≤ m ≤ n ≤ d`, then + `2 * G_d(m, n) = 2 * n + (m - 1) * (2 * n - m)`. +-/ + +public section + +namespace SumOfSetsInSeveralDimensions + +open Finset + +variable {d m n : ℕ} + +/-- `G_d(m + 1, n) = G_d(m, n) + min d (n - m)` for `m ≥ 1`. -/ +lemma sumsetCardLowerBound_add_one (hm : 1 ≤ m) : + sumsetCardLowerBound d (m + 1) n = sumsetCardLowerBound d m n + min d (n - m) := by + obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le' hm + rw [sumsetCardLowerBound_eq, sumsetCardLowerBound_eq, Nat.add_sub_cancel, Nat.add_sub_cancel, + sum_Icc_succ_top (by grind)] + grind + +/-- **Formula (1.5).** If `m + d ≤ n + 1`, then `G_d(m, n) = n + d * (m - 1)`. -/ +lemma sumsetCardLowerBound_of_add_le (h : m + d ≤ n + 1) : + sumsetCardLowerBound d m n = n + d * (m - 1) := by + rw [sumsetCardLowerBound_eq, sum_const_nat (m := d) (by grind), Nat.card_Icc] + grind + +/-- **Formula (1.6).** If `m ≤ n < m + d` and `d < n`, then +`2 * G_d(m, n) + d * (d + 1) + (n - m) * (n - m + 1) = 2 * n * (d + 1)`. -/ +lemma two_mul_sumsetCardLowerBound_add_add (hmn : m ≤ n) (hnm : n < m + d) (hdn : d < n) : + 2 * sumsetCardLowerBound d m n + d * (d + 1) + (n - m) * (n - m + 1) = 2 * n * (d + 1) := by + induction m, (by grind : n + 1 - d ≤ m) using Nat.le_induction with + | base => + rw [sumsetCardLowerBound_of_add_le (by grind)] + obtain ⟨c, rfl⟩ := Nat.exists_eq_add_of_lt hdn + obtain ⟨e, rfl⟩ := Nat.exists_eq_add_of_le' (by grind : 1 ≤ d) + rw [(by grind : e + 1 + c + 1 + 1 - (e + 1) - 1 = c + 1), + (by grind : e + 1 + c + 1 - (e + 1 + c + 1 + 1 - (e + 1)) = e)] + ring + | succ m hm ih => + obtain ⟨t, rfl⟩ := Nat.exists_eq_add_of_lt hmn + rw [sumsetCardLowerBound_add_one (by grind), (by grind : m + t + 1 - (m + 1) = t), + (by grind : min d (m + t + 1 - m) = t + 1)] + rw [(by grind : m + t + 1 - m = t + 1)] at ih + nlinarith [ih (by grind) (by grind)] + +/-- **Formula (1.6), first form.** If `m ≤ n < m + d` and `d < n`, then +`2 * G_d(m, n) + (d - t) * (d - t - 1) = 2 * (n + d * (m - 1))`, where `t = n - m`. -/ +lemma two_mul_sumsetCardLowerBound_add (hmn : m ≤ n) (hnm : n < m + d) (hdn : d < n) : + 2 * sumsetCardLowerBound d m n + (d - (n - m)) * (d - (n - m) - 1) = + 2 * (n + d * (m - 1)) := by + have h := two_mul_sumsetCardLowerBound_add_add hmn hnm hdn + obtain ⟨t, rfl⟩ := Nat.exists_eq_add_of_le hmn + obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt (by grind : t < d) + obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_le' (by grind : 1 ≤ m) + rw [Nat.add_sub_cancel_left] at h + rw [Nat.add_sub_cancel_left, (by grind : t + k + 1 - t = k + 1), Nat.add_sub_cancel, + Nat.add_sub_cancel] + nlinarith [h] + +/-- **Formula (1.7).** If `1 ≤ m ≤ n ≤ d`, then `2 * G_d(m, n) = 2 * n + (m - 1) * (2 * n - m)`. -/ +lemma two_mul_sumsetCardLowerBound_of_le (hm : 1 ≤ m) (hmn : m ≤ n) (hnd : n ≤ d) : + 2 * sumsetCardLowerBound d m n = 2 * n + (m - 1) * (2 * n - m) := by + induction m, hm using Nat.le_induction with + | base => simp [sumsetCardLowerBound_eq] + | succ m hm ih => + obtain ⟨t, rfl⟩ := Nat.exists_eq_add_of_lt hmn + rw [sumsetCardLowerBound_add_one hm, (by grind : min d (m + t + 1 - m) = t + 1), + Nat.add_sub_cancel, (by grind : 2 * (m + t + 1) - (m + 1) = m + 2 * t + 1)] + rw [(by grind : 2 * (m + t + 1) - m = m + 2 * t + 2)] at ih + obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le' hm + rw [Nat.add_sub_cancel] at ih + nlinarith [ih (by grind)] + +end SumOfSetsInSeveralDimensions diff --git a/LeanPool/SumOfSetsInSeveralDimensions/MinCardAdd.lean b/LeanPool/SumOfSetsInSeveralDimensions/MinCardAdd.lean new file mode 100644 index 0000000000..b1635f86c1 --- /dev/null +++ b/LeanPool/SumOfSetsInSeveralDimensions/MinCardAdd.lean @@ -0,0 +1,111 @@ +/- +Copyright (c) 2026 Gabriel Dahia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Dahia +-/ +module + +public import LeanPool.SumOfSetsInSeveralDimensions.AffineDim +public import LeanPool.SumOfSetsInSeveralDimensions.LowerBoundFunction +public import Mathlib.Algebra.Group.Pointwise.Finset.Basic +public import Mathlib.Order.ConditionallyCompleteLattice.Basic +import Mathlib.Order.Lattice.Nat +import LeanPool.SumOfSetsInSeveralDimensions.AffineDimSumset +import LeanPool.SumOfSetsInSeveralDimensions.Construction +import LeanPool.SumOfSetsInSeveralDimensions.LowerBound + +/-! +# The least size of a sumset in `ℝ^d` + +Ruzsa's paper defines `F_d(m, n)` as the least `|A + B|` over sets `A, B ⊆ ℝ^d` with `|A| = m`, +`|B| = n` and `A + B` of affine dimension `d`, and `F'_d(m, n)` as the same minimum with `B` of +affine dimension `d` instead. Theorem 2 of the paper states that `F_d(m, n) = F'_d(m, n) = +G_d(m, n)` for `1 ≤ m ≤ n`, unless `n < d + 1` or `m ≤ n - m ≤ d`. The sets of Section 3 attain +`G_d(m, n)` for all `1 ≤ m ≤ n` with `d + 1 ≤ n`, so the equalities hold for these pairs, which +include those excluded by the second condition. + +## Main definitions + +* `minCardAdd d m n`: the function `F_d(m, n)`. +* `minCardAddOfDimRight d m n`: the function `F'_d(m, n)`. + +## Main statements + +* `minCardAdd_eq_sumsetCardLowerBound`, `minCardAddOfDimRight_eq_sumsetCardLowerBound`: Theorem 2. +* `sInf_card_add_eq_add_sum_min`, `sInf_card_add_of_finrank_span_sub_right_eq_add_sum_min`: + Theorem 2 with `F_d`, `F'_d` and `G_d` unfolded and the affine dimension written as the + dimension of the span of the differences. +-/ + +@[expose] public section + +namespace SumOfSetsInSeveralDimensions + +open Finset +open scoped Pointwise + +/-- `F_d(m, n)`: the least size of `A + B` for `A, B ⊆ ℝ^d` with `|A| = m`, `|B| = n` and `A + B` +of affine dimension `d`. -/ +noncomputable def minCardAdd (d m n : ℕ) : ℕ := + sInf {k | ∃ A B : Finset (Fin d → ℝ), #A = m ∧ #B = n ∧ (A + B).affineDim = d ∧ + #(A + B) = k} + +/-- `F'_d(m, n)`: the least size of `A + B` for `A, B ⊆ ℝ^d` with `|A| = m`, `|B| = n` and `B` +of affine dimension `d`. -/ +noncomputable def minCardAddOfDimRight (d m n : ℕ) : ℕ := + sInf {k | ∃ A B : Finset (Fin d → ℝ), #A = m ∧ #B = n ∧ B.affineDim = d ∧ #(A + B) = k} + +variable {d m n : ℕ} + +private lemma sumsetCardLowerBound_le_card_add {A B : Finset (Fin d → ℝ)} (hm : 1 ≤ m) + (hmn : m ≤ n) (hA : #A = m) (hB : #B = n) (hdim : (A + B).affineDim = d) : + sumsetCardLowerBound d m n ≤ #(A + B) := by + have h := card_add_sum_min_le_card_add (d := d) (A := B) (B := A) (card_pos.1 (by grind)) + (by grind) (by rwa [add_comm]) + rwa [add_comm B, hA, hB, ← sumsetCardLowerBound_eq] at h + +/-- **Theorem 2 of Ruzsa, for `F_d`.** For `1 ≤ d`, `1 ≤ m ≤ n` and `d + 1 ≤ n`, +`F_d(m, n) = G_d(m, n)`. -/ +theorem minCardAdd_eq_sumsetCardLowerBound (hd : 1 ≤ d) (hm : 1 ≤ m) (hmn : m ≤ n) + (hn : d + 1 ≤ n) : minCardAdd d m n = sumsetCardLowerBound d m n := by + obtain ⟨A, B, hA, hB, hBdim, hAB⟩ := exists_card_add_eq_sumsetCardLowerBound hd hm hmn hn + have hdim : (A + B).affineDim = d := by + rw [add_comm] + exact affineDim_add_eq_of_left_eq (card_pos.1 (by grind)) hBdim + refine le_antisymm (Nat.sInf_le ⟨A, B, hA, hB, hdim, hAB⟩) + (le_csInf ⟨_, A, B, hA, hB, hdim, rfl⟩ ?_) + rintro k ⟨A', B', hA', hB', hdim', rfl⟩ + exact sumsetCardLowerBound_le_card_add hm hmn hA' hB' hdim' + +/-- **Theorem 2 of Ruzsa, for `F'_d`.** For `1 ≤ d`, `1 ≤ m ≤ n` and `d + 1 ≤ n`, +`F'_d(m, n) = G_d(m, n)`. -/ +theorem minCardAddOfDimRight_eq_sumsetCardLowerBound (hd : 1 ≤ d) (hm : 1 ≤ m) (hmn : m ≤ n) + (hn : d + 1 ≤ n) : minCardAddOfDimRight d m n = sumsetCardLowerBound d m n := by + obtain ⟨A, B, hA, hB, hBdim, hAB⟩ := exists_card_add_eq_sumsetCardLowerBound hd hm hmn hn + refine le_antisymm (Nat.sInf_le ⟨A, B, hA, hB, hBdim, hAB⟩) + (le_csInf ⟨_, A, B, hA, hB, hBdim, rfl⟩ ?_) + rintro k ⟨A', B', hA', hB', hBdim', rfl⟩ + refine sumsetCardLowerBound_le_card_add hm hmn hA' hB' ?_ + rw [add_comm] + exact affineDim_add_eq_of_left_eq (card_pos.1 (by grind)) hBdim' + +/-- Theorem 2 of Ruzsa for `F_d`, with `F_d` and `G_d` unfolded and the affine dimension of +`A + B` written as the dimension of the span of `(A + B) - (A + B)`. -/ +theorem sInf_card_add_eq_add_sum_min (hd : 1 ≤ d) (hm : 1 ≤ m) (hmn : m ≤ n) (hn : d + 1 ≤ n) : + sInf {k | ∃ A B : Finset (Fin d → ℝ), #A = m ∧ #B = n ∧ + Module.finrank ℝ (Submodule.span ℝ (↑(A + B) - ↑(A + B) : Set (Fin d → ℝ))) = d ∧ + #(A + B) = k} = n + ∑ j ∈ Icc 1 (m - 1), min d (n - j) := by + simp_rw [← affineDim_eq_finrank_span_sub, ← sumsetCardLowerBound_eq] + exact minCardAdd_eq_sumsetCardLowerBound hd hm hmn hn + +/-- Theorem 2 of Ruzsa for `F'_d`, with `F'_d` and `G_d` unfolded and the affine dimension of `B` +written as the dimension of the span of `B - B`. -/ +theorem sInf_card_add_of_finrank_span_sub_right_eq_add_sum_min (hd : 1 ≤ d) (hm : 1 ≤ m) + (hmn : m ≤ n) (hn : d + 1 ≤ n) : + sInf {k | ∃ A B : Finset (Fin d → ℝ), #A = m ∧ #B = n ∧ + Module.finrank ℝ (Submodule.span ℝ (↑B - ↑B : Set (Fin d → ℝ))) = d ∧ #(A + B) = k} = + n + ∑ j ∈ Icc 1 (m - 1), min d (n - j) := by + simp_rw [← affineDim_eq_finrank_span_sub, ← sumsetCardLowerBound_eq] + exact minCardAddOfDimRight_eq_sumsetCardLowerBound hd hm hmn hn + +end SumOfSetsInSeveralDimensions diff --git a/LeanPool/SumOfSetsInSeveralDimensions/Normalize.lean b/LeanPool/SumOfSetsInSeveralDimensions/Normalize.lean new file mode 100644 index 0000000000..585b131af4 --- /dev/null +++ b/LeanPool/SumOfSetsInSeveralDimensions/Normalize.lean @@ -0,0 +1,97 @@ +/- +Copyright (c) 2026 Gabriel Dahia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Dahia +-/ +module + +public import LeanPool.SumOfSetsInSeveralDimensions.AffineDim +public import Mathlib.Algebra.Group.Pointwise.Finset.Basic +public import Mathlib.Algebra.Order.Group.PiLex +import Mathlib.Tactic.Abel + +/-! +# Translating a set so that its lexicographic minimum is the origin + +Order `ℝ^D` lexicographically. The translate `normalize S` of a nonempty finite set `S` by minus +its least element contains `0`, and its other elements are positive. Cardinalities of sets and +sumsets and the affine dimension of a sumset do not change under this translation. +-/ + +public section + +namespace SumOfSetsInSeveralDimensions + +open Finset +open scoped Pointwise + +variable {D : ℕ} + +private noncomputable def lexMin (S : Finset (Fin D → ℝ)) (hS : S.Nonempty) : Fin D → ℝ := + ofLex ((S.image toLex).min' (hS.image toLex)) + +private lemma lexMin_mem {S : Finset (Fin D → ℝ)} (hS : S.Nonempty) : lexMin S hS ∈ S := by + obtain ⟨x, hx, hxmin⟩ := mem_image.1 (min'_mem (S.image toLex) (hS.image toLex)) + rwa [lexMin, ← hxmin, ofLex_toLex] + +private lemma lexMin_le {S : Finset (Fin D → ℝ)} (hS : S.Nonempty) {x : Fin D → ℝ} + (hx : x ∈ S) : toLex (lexMin S hS) ≤ toLex x := by + rw [lexMin, toLex_ofLex] + exact min'_le _ _ (mem_image_of_mem toLex hx) + +private lemma lexMin_sub_pos {S : Finset (Fin D → ℝ)} (hS : S.Nonempty) + {x : Fin D → ℝ} (hx : x ∈ S) (hne : x ≠ lexMin S hS) : + 0 < toLex (x - lexMin S hS) := by + rw [toLex_sub, sub_pos] + apply (lexMin_le hS hx).lt_of_ne + simpa using hne.symm + +/-- The translate of a nonempty finite set `S ⊆ ℝ^D` by minus its lexicographically least +element. -/ +noncomputable def normalize (S : Finset (Fin D → ℝ)) (hS : S.Nonempty) : Finset (Fin D → ℝ) := + S.image fun x ↦ x - lexMin S hS + +/-- Translation does not change the number of points. -/ +lemma normalize_card {S : Finset (Fin D → ℝ)} (hS : S.Nonempty) : #(normalize S hS) = #S := + card_image_of_injective _ (sub_left_injective (b := lexMin S hS)) + +/-- The translated set contains the origin. -/ +lemma zero_mem_normalize {S : Finset (Fin D → ℝ)} (hS : S.Nonempty) : 0 ∈ normalize S hS := + mem_image.2 ⟨lexMin S hS, lexMin_mem hS, sub_self _⟩ + +/-- The translated set is nonempty. -/ +lemma normalize_nonempty {S : Finset (Fin D → ℝ)} (hS : S.Nonempty) : + (normalize S hS).Nonempty := + ⟨0, zero_mem_normalize hS⟩ + +/-- The nonzero elements of the translated set are lexicographically positive. -/ +lemma normalize_pos_of_ne_zero {S : Finset (Fin D → ℝ)} (hS : S.Nonempty) + {x : Fin D → ℝ} (hx : x ∈ normalize S hS) (hx0 : x ≠ 0) : 0 < toLex x := by + obtain ⟨y, hy, rfl⟩ := mem_image.1 hx + apply lexMin_sub_pos hS hy + rintro rfl + exact hx0 (sub_self _) + +private lemma normalize_add {A B : Finset (Fin D → ℝ)} (hA : A.Nonempty) (hB : B.Nonempty) : + normalize A hA + normalize B hB = + (A + B).image fun x ↦ x - (lexMin A hA + lexMin B hB) := by + ext x + simp only [normalize, mem_add, mem_image] + constructor + · rintro ⟨_, ⟨a, ha, rfl⟩, _, ⟨b, hb, rfl⟩, rfl⟩ + exact ⟨a + b, ⟨a, ha, b, hb, rfl⟩, by abel⟩ + · rintro ⟨_, ⟨a, ha, b, hb, rfl⟩, rfl⟩ + exact ⟨a - lexMin A hA, ⟨a, ha, rfl⟩, b - lexMin B hB, ⟨b, hb, rfl⟩, by abel⟩ + +/-- The sum of the translates of `A` and `B` has as many points as `A + B`. -/ +lemma normalize_add_card {A B : Finset (Fin D → ℝ)} (hA : A.Nonempty) (hB : B.Nonempty) : + #(normalize A hA + normalize B hB) = #(A + B) := by + rw [normalize_add] + exact card_image_of_injective _ sub_left_injective + +/-- The sum of the translates of `A` and `B` has the affine dimension of `A + B`. -/ +lemma normalize_add_dim {A B : Finset (Fin D → ℝ)} (hA : A.Nonempty) (hB : B.Nonempty) : + (normalize A hA + normalize B hB).affineDim = (A + B).affineDim := by + rw [normalize_add, affineDim_image_sub] + +end SumOfSetsInSeveralDimensions diff --git a/LeanPool/projects/sum-of-sets-in-several-dimensions.yaml b/LeanPool/projects/sum-of-sets-in-several-dimensions.yaml new file mode 100644 index 0000000000..52fcb589d6 --- /dev/null +++ b/LeanPool/projects/sum-of-sets-in-several-dimensions.yaml @@ -0,0 +1,68 @@ +slug: sum-of-sets-in-several-dimensions +title: Sum of sets in several dimensions +summary: Proves Ruzsa's lower bound for sumsets in R^D. If A and B are finite with B + nonempty, |B| ≤ |A| and A + B of affine dimension d, then + |A + B| ≥ |A| + Σ_{t=1}^{|B|-1} min(d, |A| - t), and this bound is attained in R^d + whenever d ≥ 1 and |A| ≥ d + 1, so it is the exact minimum. Derives the asymmetric + form of Freiman's lemma, |A + B| ≥ |A| + d|B| - d(d+1)/2. Defines the Freiman + dimension of a finite subset of a commutative monoid, transfers the bound to sets + with a Freiman model in R^r, and shows that a set X with |X + X| ≤ κ|X| has Freiman + dimension at most 2κ - 1 and at most κ - 1 + κ(2κ - 1)/|X|. +branch: additive combinatorics +entry_module: LeanPool.SumOfSetsInSeveralDimensions +authors: +- Gabriel Dahia +source: + title: Sum of sets in several dimensions + authors: + - Imre Z. Ruzsa + doi: 10.1007/BF01302969 + url: https://github.com/gdahia/SumOfSetsInSeveralDimensions/tree/bd2694b89fbe18ee5c4365a6330eba36d9f7ed8e + github_repo: gdahia/SumOfSetsInSeveralDimensions + commit: bd2694b89fbe18ee5c4365a6330eba36d9f7ed8e +license: Apache-2.0 +status: verified +provenance: AI +main_declarations: +- SumOfSetsInSeveralDimensions.card_add_sum_min_le_card_add_of_finrank_span_sub_eq +- SumOfSetsInSeveralDimensions.card_add_mul_card_le_card_add_add_of_le_finrank_span_sub +- SumOfSetsInSeveralDimensions.sInf_card_add_eq_add_sum_min +- SumOfSetsInSeveralDimensions.freimanDim_le_two_mul_sub_one_of_card_add_le +main_results: +- declaration: SumOfSetsInSeveralDimensions.card_add_sum_min_le_card_add_of_finrank_span_sub_eq + informal: For finite A, B ⊆ R^D with B nonempty and |B| ≤ |A|, if the differences + of A + B span a space of dimension d, then + |A| + Σ_{t=1}^{|B|-1} min(d, |A| - t) ≤ |A + B|. + source_ref: Theorem 1. +- declaration: SumOfSetsInSeveralDimensions.card_add_mul_card_le_card_add_add_of_le_finrank_span_sub + informal: For finite A, B ⊆ R^D with B nonempty and |B| ≤ |A|, and every d at most + the dimension of the span of the differences of A + B, + |A| + d|B| ≤ |A + B| + d(d+1)/2. + source_ref: Corollary 1.1. +- declaration: SumOfSetsInSeveralDimensions.sInf_card_add_eq_add_sum_min + informal: For d ≥ 1, 1 ≤ m ≤ n and n ≥ d + 1, the least size of A + B over + A, B ⊆ R^d with |A| = m, |B| = n and A + B of affine dimension d is + n + Σ_{j=1}^{m-1} min(d, n - j). + source_ref: Theorem 2, F_d(m, n) = G_d(m, n). +- declaration: SumOfSetsInSeveralDimensions.sInf_card_add_of_finrank_span_sub_right_eq_add_sum_min + informal: The same minimum n + Σ_{j=1}^{m-1} min(d, n - j) holds when only B is + required to have affine dimension d. + source_ref: Theorem 2, F'_d(m, n) = G_d(m, n). +- declaration: SumOfSetsInSeveralDimensions.freimanDim_le_two_mul_sub_one_of_card_add_le + informal: A nonempty finite subset X of a cancellative commutative monoid with + |X + X| ≤ κ|X|, for a real κ, has Freiman dimension at most 2κ - 1. +- declaration: SumOfSetsInSeveralDimensions.freimanDim_le_sub_one_add_mul_div_card_of_card_add_le + informal: Under the same hypotheses, the Freiman dimension of X is at most + κ - 1 + κ(2κ - 1)/|X|. +- declaration: SumOfSetsInSeveralDimensions.card_add_sum_min_le_of_freimanDim_union + informal: Ruzsa's lower bound holds for finite A, B in a commutative monoid with + d replaced by r - 1, where r ≥ 1 is the Freiman dimension of A ∪ B. +tags: +- additive-combinatorics +- sumsets +- freiman-dimension +- discrete-geometry +msc: +- 11P70 +- 11B13 +- 11B75 From e3d4e889a2fcdf28c150a42d9ac2677aa764e9b9 Mon Sep 17 00:00:00 2001 From: Gabriel Dahia Date: Sun, 8 Nov 2026 16:04:46 -0300 Subject: [PATCH 2/2] Update LeanPool/projects/sum-of-sets-in-several-dimensions.yaml Co-authored-by: greptile-apps[bot] <165735046+greptile-apps[bot]@users.noreply.github.com> --- LeanPool/projects/sum-of-sets-in-several-dimensions.yaml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/LeanPool/projects/sum-of-sets-in-several-dimensions.yaml b/LeanPool/projects/sum-of-sets-in-several-dimensions.yaml index 52fcb589d6..89e500b909 100644 --- a/LeanPool/projects/sum-of-sets-in-several-dimensions.yaml +++ b/LeanPool/projects/sum-of-sets-in-several-dimensions.yaml @@ -56,7 +56,8 @@ main_results: κ - 1 + κ(2κ - 1)/|X|. - declaration: SumOfSetsInSeveralDimensions.card_add_sum_min_le_of_freimanDim_union informal: Ruzsa's lower bound holds for finite A, B in a commutative monoid with - d replaced by r - 1, where r ≥ 1 is the Freiman dimension of A ∪ B. + B nonempty and |B| ≤ |A|, with d replaced by r - 1, where r ≥ 1 is the Freiman + dimension of A ∪ B. tags: - additive-combinatorics - sumsets