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..89e500b909 --- /dev/null +++ b/LeanPool/projects/sum-of-sets-in-several-dimensions.yaml @@ -0,0 +1,69 @@ +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 + 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 +- freiman-dimension +- discrete-geometry +msc: +- 11P70 +- 11B13 +- 11B75