Import Ruzsa's sum of sets in several dimensions

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.
+-/

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

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

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