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

theorem SumOfSetsInSeveralDimensions.two_mul_mul_le_two_mul_sum_min_add (d : ℕ) {m n : ℕ} (hm : 1 ≤ m) (hmn : m ≤ n) : 2 * (d * m) ≤ 2 * ∑ t ∈ Finset.Icc 1 (m - 1), min d (n - t) + d * (d + 1)

For 1 ≤ m ≤ n, twice the sum ∑ t ∈ {1, …, m - 1}, min d (n - t) is at least 2 * d * m - d * (d + 1).

theorem SumOfSetsInSeveralDimensions.two_mul_card_add_mul_card_le {D d : ℕ} {A B : Finset (Fin D → ℝ)} (hB : B.Nonempty) (hBA : B.card ≤ A.card) (hd : d ≤ (A + B).affineDim) : 2 * (A.card + d * B.card) ≤ 2 * (A + B).card + d * (d + 1)

The closed form of Ruzsa's bound, multiplied by two: 2 * (|A| + d * |B|) is at most 2 * |A + B| + d * (d + 1).

theorem SumOfSetsInSeveralDimensions.card_add_mul_card_le_card_add_add {D d : ℕ} {A B : Finset (Fin D → ℝ)} (hB : B.Nonempty) (hBA : B.card ≤ A.card) (hd : d ≤ (A + B).affineDim) : A.card + d * B.card ≤ (A + B).card + d * (d + 1) / 2

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 SumOfSetsInSeveralDimensions.card_add_mul_card_le_card_add_add_of_le_finrank_span_sub {D d : ℕ} {A B : Finset (Fin D → ℝ)} (hB : B.Nonempty) (hBA : B.card ≤ A.card) (hd : d ≤ Module.finrank ℝ ↥(Submodule.span ℝ (↑(A + B) - ↑(A + B)))) : A.card + d * B.card ≤ (A + B).card + d * (d + 1) / 2

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 SumOfSetsInSeveralDimensions.card_add_mul_card_sub_le_card_add {D d : ℕ} {A B : Finset (Fin D → ℝ)} (hB : B.Nonempty) (hBA : B.card ≤ A.card) (hd : d ≤ (A + B).affineDim) : ↑A.card + ↑d * ↑B.card - ↑d * (↑d + 1) / 2 ≤ ↑(A + B).card

The asymmetric form of Freiman's lemma in ℝ: |A| + d * |B| - d * (d + 1) / 2 ≤ |A + B|.

theorem SumOfSetsInSeveralDimensions.max_card_add_mul_min_card_le_card_add_add {D d : ℕ} {A B : Finset (Fin D → ℝ)} (hA : A.Nonempty) (hB : B.Nonempty) (hd : d ≤ (A + B).affineDim) : max A.card B.card + d * min A.card B.card ≤ (A + B).card + d * (d + 1) / 2

The asymmetric form of Freiman's lemma without an assumption on which set is larger.