Sumset bounds from the Freiman dimension

Let A and B be finite subsets of a commutative monoid with B nonempty and |B| ≤ |A|, and let f be a Freiman isomorphism of order 2 from A ∪ B onto a subset of ℝ^r of affine dimension r. Then f sends A and B to sets A' and B' with |A'| = |A|, |B'| = |B| and |A' + B'| = |A + B|, and A' + B' has affine dimension at least r - 1. Ruzsa's theorem then gives |A| + ∑ t ∈ {1, …, |B| - 1}, min (r - 1) (|A| - t) ≤ |A + B|. A Freiman model in ℚ^r is one in ℝ^r, so this holds when r ≥ 1 is the Freiman dimension of A ∪ B.

For A = B = X the model f(X) + f(X) has affine dimension r, and the asymmetric form of Freiman's lemma gives (r + 1) * |X| - r * (r + 1) / 2 ≤ |X + X|. If |X + X| ≤ κ * |X|, then r ≤ 2 * κ - 1, so r * (r + 1) / 2 ≤ κ * (2 * κ - 1) and r ≤ κ - 1 + κ * (2 * κ - 1) / |X|.

Main statements

• card_add_sum_min_le_card_add_of_isAddFreimanIso: the bound above.
• card_add_sum_min_le_of_freimanDim_union: the bound for r the Freiman dimension of A ∪ B.
• two_mul_card_add_mul_card_le_of_isAddFreimanIso: Freiman's lemma for a Freiman model f of X in ℝ^r of affine dimension r, 2 * (|X| + r * |X|) ≤ 2 * |X + X| + r * (r + 1).
• card_add_mul_card_sub_choose_le_card_add_of_freimanDim_union: the weaker bound |A| + (r - 1) * |B| - (r + 1).choose 2 ≤ |A + B|.
• card_add_mul_card_sub_le_card_add_of_freimanDim: if X is nonempty with Freiman dimension r ≥ 1, then |X| + r * |X| - r * (r + 1) / 2 ≤ |X + X|.
• le_two_mul_sub_one_of_isAddFreimanIso: if |X + X| ≤ κ * |X| for a real κ, then a Freiman model of X in ℝ^r of affine dimension r has r ≤ 2 * κ - 1.
• freimanDim_le_two_mul_sub_one_of_card_add_le: if |X + X| ≤ κ * |X|, then freimanDim X ≤ 2 * κ - 1.
• le_sub_one_add_mul_div_card_of_isAddFreimanIso: under the same hypotheses, r ≤ κ - 1 + κ * (2 * κ - 1) / |X|.
• freimanDim_le_sub_one_add_mul_div_card_of_card_add_le: if |X + X| ≤ κ * |X|, then freimanDim X ≤ κ - 1 + κ * (2 * κ - 1) / |X|.

theorem SumOfSetsInSeveralDimensions.rationalVectorToReal_injective {d : ℕ} : Function.Injective rationalVectorToReal

theorem SumOfSetsInSeveralDimensions.rationalVectorToReal_add {d : ℕ} (x y : Fin d → ℚ) : rationalVectorToReal (x + y) = rationalVectorToReal x + rationalVectorToReal y

theorem SumOfSetsInSeveralDimensions.isAddFreimanIso_rationalVectorToReal_comp {G : Type u_1} [AddCommMonoid G] {d : ℕ} {X : Finset G} {f : G → Fin d → ℚ} (hf : IsAddFreimanIso 2 (↑X) (↑(Finset.image f X)) f) : IsAddFreimanIso 2 (↑X) (↑(Finset.image (rationalVectorToReal ∘ f) X)) (rationalVectorToReal ∘ f)

A Freiman isomorphism into ℚ^d followed by the inclusion of ℚ^d into ℝ^d is a Freiman isomorphism into ℝ^d.

theorem SumOfSetsInSeveralDimensions.exists_isAddFreimanIso_of_freimanDim_eq {G : Type u_1} [AddCommMonoid G] {r : ℕ} {X : Finset G} (hdim : freimanDim X = r) (hr : r ≠ 0) : ∃ (f : G → Fin r → ℝ), IsAddFreimanIso 2 (↑X) (↑(Finset.image f X)) f ∧ (Finset.image f X).affineDim = r

A set of Freiman dimension r ≥ 1 has a Freiman model in ℝ^r of affine dimension r.

theorem SumOfSetsInSeveralDimensions.card_image_eq_of_kernel_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] [DecidableEq γ] {s : Finset α} {f : α → β} {g : α → γ} (h : ∀ x ∈ s, ∀ y ∈ s, f x = f y ↔ g x = g y) : (Finset.image f s).card = (Finset.image g s).card

Two maps with the same fibres on s have images of s of the same size.

theorem SumOfSetsInSeveralDimensions.card_add_image_of_isAddFreimanIso {G : Type u_1} {H : Type u_2} [DecidableEq G] [DecidableEq H] [AddCommMonoid G] [AddCommMonoid H] {X A B : Finset G} {f : G → H} (hf : IsAddFreimanIso 2 (↑X) (↑(Finset.image f X)) f) (hAX : A ⊆ X) (hBX : B ⊆ X) : (Finset.image f A + Finset.image f B).card = (A + B).card

A Freiman isomorphism of order 2 on X preserves the size of A + B for A, B ⊆ X.

theorem SumOfSetsInSeveralDimensions.card_add_sum_min_le_card_add_of_isAddFreimanIso {G : Type u_1} [DecidableEq G] [AddCommMonoid G] {r : ℕ} {A B : Finset G} {f : G → Fin r → ℝ} (hB : B.Nonempty) (hBA : B.card ≤ A.card) (hf : IsAddFreimanIso 2 (↑(A ∪ B)) (↑(Finset.image f (A ∪ B))) f) (hdim : (Finset.image f (A ∪ B)).affineDim = r) : A.card + ∑ t ∈ Finset.Icc 1 (B.card - 1), min (r - 1) (A.card - t) ≤ (A + B).card

Ruzsa's theorem for a Freiman model. Let A and B be finite subsets of a commutative monoid with B nonempty and |B| ≤ |A|, and let f be a Freiman isomorphism of order 2 from A ∪ B onto a subset of ℝ^r of affine dimension r. Then |A| + ∑ t ∈ {1, …, |B| - 1}, min (r - 1) (|A| - t) ≤ |A + B|.

theorem SumOfSetsInSeveralDimensions.card_add_sum_min_le_card_add_of_isAddFreimanIso_of_finrank_span_sub_eq {G : Type u_1} [DecidableEq G] [AddCommMonoid G] {r : ℕ} {A B : Finset G} {f : G → Fin r → ℝ} (hB : B.Nonempty) (hBA : B.card ≤ A.card) (hf : IsAddFreimanIso 2 (↑(A ∪ B)) (↑(Finset.image f (A ∪ B))) f) (hdim : Module.finrank ℝ ↥(Submodule.span ℝ (↑(Finset.image f (A ∪ B)) - ↑(Finset.image f (A ∪ B)))) = r) : A.card + ∑ t ∈ Finset.Icc 1 (B.card - 1), min (r - 1) (A.card - t) ≤ (A + B).card

Ruzsa's theorem for a Freiman model, with the affine dimension of the model written as the dimension of the span of its differences.

theorem SumOfSetsInSeveralDimensions.two_mul_card_add_mul_card_le_of_isAddFreimanIso {G : Type u_1} [DecidableEq G] [AddCommMonoid G] {r : ℕ} {X : Finset G} {f : G → Fin r → ℝ} (hX : X.Nonempty) (hf : IsAddFreimanIso 2 (↑X) (↑(Finset.image f X)) f) (hdim : (Finset.image f X).affineDim = r) : 2 * (X.card + r * X.card) ≤ 2 * (X + X).card + r * (r + 1)

Freiman's lemma for a Freiman model. If f is a Freiman isomorphism of order 2 from a nonempty X onto a subset of ℝ^r of affine dimension r, then 2 * (|X| + r * |X|) ≤ 2 * |X + X| + r * (r + 1).

theorem SumOfSetsInSeveralDimensions.le_two_mul_sub_one_of_isAddFreimanIso {G : Type u_1} [DecidableEq G] [AddCancelCommMonoid G] {r : ℕ} {κ : ℝ} {X : Finset G} {f : G → Fin r → ℝ} (hX : X.Nonempty) (hXX : ↑(X + X).card ≤ κ * ↑X.card) (hf : IsAddFreimanIso 2 (↑X) (↑(Finset.image f X)) f) (hdim : (Finset.image f X).affineDim = r) : ↑r ≤ 2 * κ - 1

If |X + X| ≤ κ * |X| for a nonempty X and f is a Freiman isomorphism of order 2 from X onto a subset of ℝ^r of affine dimension r, then r ≤ 2 * κ - 1.

theorem SumOfSetsInSeveralDimensions.le_two_mul_sub_one_of_isAddFreimanIso_of_finrank_span_sub_eq {G : Type u_1} [DecidableEq G] [AddCancelCommMonoid G] {r : ℕ} {κ : ℝ} {X : Finset G} {f : G → Fin r → ℝ} (hX : X.Nonempty) (hXX : ↑(X + X).card ≤ κ * ↑X.card) (hf : IsAddFreimanIso 2 (↑X) (↑(Finset.image f X)) f) (hdim : Module.finrank ℝ ↥(Submodule.span ℝ (↑(Finset.image f X) - ↑(Finset.image f X))) = r) : ↑r ≤ 2 * κ - 1

The bound r ≤ 2 * κ - 1 for a Freiman model, with the affine dimension of the model written as the dimension of the span of its differences.

theorem SumOfSetsInSeveralDimensions.sub_mul_sub_choose_le_sum_min (b r : ℕ) : (r - 1) * b - (r + 1).choose 2 ≤ ∑ t ∈ Finset.Icc 1 (b - 1), min (r - 1) (b - t)

theorem SumOfSetsInSeveralDimensions.sub_mul_sub_choose_le_sum_min_of_le {a b r d : ℕ} (hba : b ≤ a) (hrd : r ≤ d + 1) : (r - 1) * b - (r + 1).choose 2 ≤ ∑ t ∈ Finset.Icc 1 (b - 1), min d (a - t)

theorem SumOfSetsInSeveralDimensions.card_add_sum_min_le_of_freimanDim_union {G : Type u_1} [DecidableEq G] [AddCommMonoid G] {r : ℕ} {A B : Finset G} (hr : 1 ≤ r) (hB : B.Nonempty) (hBA : B.card ≤ A.card) (hdim : freimanDim (A ∪ B) = r) : A.card + ∑ t ∈ Finset.Icc 1 (B.card - 1), min (r - 1) (A.card - t) ≤ (A + B).card

Let A and B be finite with B nonempty and |B| ≤ |A|, and let r ≥ 1 be the Freiman dimension of A ∪ B. Then |A| + ∑ t ∈ {1, …, |B| - 1}, min (r - 1) (|A| - t) ≤ |A + B|.

theorem SumOfSetsInSeveralDimensions.card_add_mul_card_sub_choose_le_card_add_of_freimanDim_union {G : Type u_1} [DecidableEq G] [AddCommMonoid G] {r : ℕ} {A B : Finset G} (hr : 1 ≤ r) (hB : B.Nonempty) (hBA : B.card ≤ A.card) (hdim : freimanDim (A ∪ B) = r) : A.card + (r - 1) * B.card - (r + 1).choose 2 ≤ (A + B).card

Let A and B be finite with B nonempty and |B| ≤ |A|, and let r ≥ 1 be the Freiman dimension of A ∪ B. Then |A| + (r - 1) * |B| - (r + 1).choose 2 ≤ |A + B|.

theorem SumOfSetsInSeveralDimensions.card_add_mul_card_sub_le_card_add_of_freimanDim {G : Type u_1} [DecidableEq G] [AddCommMonoid G] {X : Finset G} (hX : X.Nonempty) (hr : freimanDim X ≠ 0) : (freimanDim X + 1) * X.card - freimanDim X * (freimanDim X + 1) / 2 ≤ (X + X).card

Freiman's lemma for X + X in terms of the Freiman dimension: if X is nonempty with Freiman dimension r ≥ 1, then (r + 1) * |X| - r * (r + 1) / 2 ≤ |X + X|.

theorem SumOfSetsInSeveralDimensions.freimanDim_le_two_mul_sub_one_of_card_add_le {G : Type u_1} [DecidableEq G] [AddCancelCommMonoid G] {κ : ℝ} {X : Finset G} (hX : X.Nonempty) (hXX : ↑(X + X).card ≤ κ * ↑X.card) : ↑(freimanDim X) ≤ 2 * κ - 1

If |X + X| ≤ κ * |X| for a nonempty X, then X has Freiman dimension at most 2 * κ - 1.

theorem SumOfSetsInSeveralDimensions.le_sub_one_add_mul_div_card_of_isAddFreimanIso {G : Type u_1} [DecidableEq G] [AddCancelCommMonoid G] {r : ℕ} {κ : ℝ} {X : Finset G} {f : G → Fin r → ℝ} (hX : X.Nonempty) (hXX : ↑(X + X).card ≤ κ * ↑X.card) (hf : IsAddFreimanIso 2 (↑X) (↑(Finset.image f X)) f) (hdim : (Finset.image f X).affineDim = r) : ↑r ≤ κ - 1 + κ * (2 * κ - 1) / ↑X.card

If |X + X| ≤ κ * |X| for a nonempty X and f is a Freiman isomorphism of order 2 from X onto a subset of ℝ^r of affine dimension r, then r ≤ κ - 1 + κ * (2 * κ - 1) / |X|.

theorem SumOfSetsInSeveralDimensions.le_sub_one_add_mul_div_card_of_isAddFreimanIso_of_finrank_span_sub_eq {G : Type u_1} [DecidableEq G] [AddCancelCommMonoid G] {r : ℕ} {κ : ℝ} {X : Finset G} {f : G → Fin r → ℝ} (hX : X.Nonempty) (hXX : ↑(X + X).card ≤ κ * ↑X.card) (hf : IsAddFreimanIso 2 (↑X) (↑(Finset.image f X)) f) (hdim : Module.finrank ℝ ↥(Submodule.span ℝ (↑(Finset.image f X) - ↑(Finset.image f X))) = r) : ↑r ≤ κ - 1 + κ * (2 * κ - 1) / ↑X.card

The bound r ≤ κ - 1 + κ * (2 * κ - 1) / |X| for a Freiman model, with the affine dimension of the model written as the dimension of the span of its differences.

theorem SumOfSetsInSeveralDimensions.freimanDim_le_sub_one_add_mul_div_card_of_card_add_le {G : Type u_1} [DecidableEq G] [AddCancelCommMonoid G] {κ : ℝ} {X : Finset G} (hX : X.Nonempty) (hXX : ↑(X + X).card ≤ κ * ↑X.card) : ↑(freimanDim X) ≤ κ - 1 + κ * (2 * κ - 1) / ↑X.card

If |X + X| ≤ κ * |X| for a nonempty X, then X has Freiman dimension at most κ - 1 + κ * (2 * κ - 1) / |X|.