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

theorem SumOfSetsInSeveralDimensions.card_add_sum_min_le_card_add {D d : ℕ} {A B : Finset (Fin D → ℝ)} (hB : B.Nonempty) (hBA : B.card ≤ A.card) (hdim : (A + B).affineDim = d) : A.card + ∑ t ∈ Finset.Icc 1 (B.card - 1), min d (A.card - t) ≤ (A + B).card

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 SumOfSetsInSeveralDimensions.card_add_sum_min_le_card_add_of_le {D d : ℕ} {A B : Finset (Fin D → ℝ)} (hB : B.Nonempty) (hBA : B.card ≤ A.card) (hd : d ≤ (A + B).affineDim) : A.card + ∑ t ∈ Finset.Icc 1 (B.card - 1), min d (A.card - t) ≤ (A + B).card

Ruzsa's theorem for every d at most the affine dimension of A + B.

theorem SumOfSetsInSeveralDimensions.card_add_sum_min_le_card_add_of_finrank_span_sub_eq {D d : ℕ} {A B : Finset (Fin D → ℝ)} (hB : B.Nonempty) (hBA : B.card ≤ A.card) (hdim : Module.finrank ℝ ↥(Submodule.span ℝ (↑(A + B) - ↑(A + B))) = d) : A.card + ∑ t ∈ Finset.Icc 1 (B.card - 1), min d (A.card - t) ≤ (A + B).card

Ruzsa's theorem, with the affine dimension of A + B written as the dimension of the span of (A + B) - (A + B).