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.

noncomputable def SumOfSetsInSeveralDimensions.minCardAdd (d m n : ℕ) : ℕ

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.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def SumOfSetsInSeveralDimensions.minCardAddOfDimRight (d m n : ℕ) : ℕ

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.

Equations

• SumOfSetsInSeveralDimensions.minCardAddOfDimRight d m n = sInf {k : ℕ | ∃ (A : Finset (Fin d → ℝ)) (B : Finset (Fin d → ℝ)), A.card = m ∧ B.card = n ∧ B.affineDim = d ∧ (A + B).card = k}

theorem SumOfSetsInSeveralDimensions.minCardAdd_eq_sumsetCardLowerBound {d m n : ℕ} (hd : 1 ≤ d) (hm : 1 ≤ m) (hmn : m ≤ n) (hn : d + 1 ≤ n) : minCardAdd d m n = sumsetCardLowerBound d m n

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 SumOfSetsInSeveralDimensions.minCardAddOfDimRight_eq_sumsetCardLowerBound {d m n : ℕ} (hd : 1 ≤ d) (hm : 1 ≤ m) (hmn : m ≤ n) (hn : d + 1 ≤ n) : minCardAddOfDimRight d m n = sumsetCardLowerBound d m n

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 SumOfSetsInSeveralDimensions.sInf_card_add_eq_add_sum_min {d m n : ℕ} (hd : 1 ≤ d) (hm : 1 ≤ m) (hmn : m ≤ n) (hn : d + 1 ≤ n) : sInf {k : ℕ | ∃ (A : Finset (Fin d → ℝ)) (B : Finset (Fin d → ℝ)), A.card = m ∧ B.card = n ∧ Module.finrank ℝ ↥(Submodule.span ℝ (↑(A + B) - ↑(A + B))) = d ∧ (A + B).card = k} = n + ∑ j ∈ Finset.Icc 1 (m - 1), min d (n - j)

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 SumOfSetsInSeveralDimensions.sInf_card_add_of_finrank_span_sub_right_eq_add_sum_min {d m n : ℕ} (hd : 1 ≤ d) (hm : 1 ≤ m) (hmn : m ≤ n) (hn : d + 1 ≤ n) : sInf {k : ℕ | ∃ (A : Finset (Fin d → ℝ)) (B : Finset (Fin d → ℝ)), A.card = m ∧ B.card = n ∧ Module.finrank ℝ ↥(Submodule.span ℝ (↑B - ↑B)) = d ∧ (A + B).card = k} = n + ∑ j ∈ Finset.Icc 1 (m - 1), min d (n - j)

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.