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).

noncomputable def SumOfSetsInSeveralDimensions.axisPoints (e k : ℕ) : Finset (Fin (e + 1) → ℝ)

The points i e₀ of ℝ^(e + 1) with i ≤ k.

Equations

• SumOfSetsInSeveralDimensions.axisPoints e k = Finset.image (fun (i : ℕ) => Pi.single 0 ↑i) (Finset.range (k + 1))

noncomputable def SumOfSetsInSeveralDimensions.unitVectors (e c : ℕ) : Finset (Fin (e + 1) → ℝ)

The unit vectors e_(j + 1) of ℝ^(e + 1) with j < c.

Equations

• SumOfSetsInSeveralDimensions.unitVectors e c = Finset.image (fun (j : Fin e) => Pi.single j.succ 1) {j : Fin e | ↑j < c}

noncomputable def SumOfSetsInSeveralDimensions.axisUnionBasis (e k c : ℕ) : Finset (Fin (e + 1) → ℝ)

The set {0, e₀, …, k e₀} ∪ {e₁, …, e_c} of ℝ^(e + 1).

Equations

• SumOfSetsInSeveralDimensions.axisUnionBasis e k c = SumOfSetsInSeveralDimensions.axisPoints e k ∪ SumOfSetsInSeveralDimensions.unitVectors e c

theorem SumOfSetsInSeveralDimensions.card_axisPoints (e k : ℕ) : (axisPoints e k).card = k + 1

theorem SumOfSetsInSeveralDimensions.card_unitVectors {e c : ℕ} (hc : c ≤ e) : (unitVectors e c).card = c

theorem SumOfSetsInSeveralDimensions.disjoint_axisPoints_unitVectors {e : ℕ} (k c : ℕ) : Disjoint (axisPoints e k) (unitVectors e c)

theorem SumOfSetsInSeveralDimensions.card_axisUnionBasis {e : ℕ} (k : ℕ) {c : ℕ} (hc : c ≤ e) : (axisUnionBasis e k c).card = k + 1 + c

theorem SumOfSetsInSeveralDimensions.axisPoints_mono {e k l : ℕ} (hkl : k ≤ l) : axisPoints e k ⊆ axisPoints e l

theorem SumOfSetsInSeveralDimensions.unitVectors_mono {e c c' : ℕ} (hcc' : c ≤ c') : unitVectors e c ⊆ unitVectors e c'

theorem SumOfSetsInSeveralDimensions.axisPoints_add_axisPoints_subset {e : ℕ} (k l : ℕ) : axisPoints e k + axisPoints e l ⊆ axisPoints e (k + l)

theorem SumOfSetsInSeveralDimensions.affineDim_axisUnionBasis {e k : ℕ} (hk : 1 ≤ k) : (axisUnionBasis e k e).affineDim = e + 1

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.

theorem SumOfSetsInSeveralDimensions.exists_card_add_le_sumsetCardLowerBound {e m n : ℕ} (hm : 1 ≤ m) (hmn : m ≤ n) (hn : e + 2 ≤ n) : ∃ (A : Finset (Fin (e + 1) → ℝ)) (B : Finset (Fin (e + 1) → ℝ)), A.card = m ∧ B.card = n ∧ B.affineDim = e + 1 ∧ (A + B).card ≤ sumsetCardLowerBound (e + 1) m n

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).

theorem SumOfSetsInSeveralDimensions.exists_card_add_eq_sumsetCardLowerBound {d m n : ℕ} (hd : 1 ≤ d) (hm : 1 ≤ m) (hmn : m ≤ n) (hn : d + 1 ≤ n) : ∃ (A : Finset (Fin d → ℝ)) (B : Finset (Fin d → ℝ)), A.card = m ∧ B.card = n ∧ B.affineDim = d ∧ (A + B).card = sumsetCardLowerBound d m n

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).