# mathlib3documentation

combinatorics.additive.salem_spencer

# Salem-Spencer sets and Roth numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines Salem-Spencer sets and the Roth number of a set.

A Salem-Spencer set is a set without arithmetic progressions of length 3. Equivalently, the average of any two distinct elements is not in the set.

The Roth number of a finset is the size of its biggest Salem-Spencer subset. This is a more general definition than the one often found in mathematical litterature, where the n-th Roth number is the size of the biggest Salem-Spencer subset of {0, ..., n - 1}.

## Main declarations #

• mul_salem_spencer: Predicate for a set to be multiplicative Salem-Spencer.
• add_salem_spencer: Predicate for a set to be additive Salem-Spencer.
• mul_roth_number: The multiplicative Roth number of a finset.
• add_roth_number: The additive Roth number of a finset.
• roth_number_nat: The Roth number of a natural. This corresponds to add_roth_number (finset.range n).

## TODO #

• Can add_salem_spencer_iff_eq_right be made more general?
• Generalize mul_salem_spencer.image to Freiman homs

## Tags #

Salem-Spencer, Roth, arithmetic progression, average, three-free

def add_salem_spencer {α : Type u_2} [add_monoid α] (s : set α) :
Prop

A Salem-Spencer, aka non averaging, set s in an additive monoid is a set such that the average of any two distinct elements is not in the set.

Equations
Instances for add_salem_spencer
def mul_salem_spencer {α : Type u_2} [monoid α] (s : set α) :
Prop

A multiplicative Salem-Spencer, aka non averaging, set s in a monoid is a set such that the multiplicative average of any two distinct elements is not in the set.

Equations
Instances for mul_salem_spencer
@[protected, instance]
def add_salem_spencer.decidable {α : Type u_1} [decidable_eq α] [add_monoid α] {s : finset α} :

Whether a given finset is Salem-Spencer is decidable.

Equations
@[protected, instance]
def mul_salem_spencer.decidable {α : Type u_1} [decidable_eq α] [monoid α] {s : finset α} :

Whether a given finset is Salem-Spencer is decidable.

Equations
theorem add_salem_spencer.mono {α : Type u_2} [add_monoid α] {s t : set α} (h : t s) (hs : add_salem_spencer s) :
theorem mul_salem_spencer.mono {α : Type u_2} [monoid α] {s t : set α} (h : t s) (hs : mul_salem_spencer s) :
@[simp]
theorem add_salem_spencer_empty {α : Type u_2} [add_monoid α] :
@[simp]
theorem mul_salem_spencer_empty {α : Type u_2} [monoid α] :
theorem set.subsingleton.add_salem_spencer {α : Type u_2} [add_monoid α] {s : set α} (hs : s.subsingleton) :
theorem set.subsingleton.mul_salem_spencer {α : Type u_2} [monoid α] {s : set α} (hs : s.subsingleton) :
@[simp]
theorem mul_salem_spencer_singleton {α : Type u_2} [monoid α] (a : α) :
@[simp]
theorem add_salem_spencer_singleton {α : Type u_2} [add_monoid α] (a : α) :
theorem add_salem_spencer.prod {α : Type u_2} {β : Type u_3} [add_monoid α] [add_monoid β] {s : set α} {t : set β} (hs : add_salem_spencer s) (ht : add_salem_spencer t) :
theorem mul_salem_spencer.prod {α : Type u_2} {β : Type u_3} [monoid α] [monoid β] {s : set α} {t : set β} (hs : mul_salem_spencer s) (ht : mul_salem_spencer t) :
theorem add_salem_spencer_pi {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), add_monoid (α i)] {s : Π (i : ι), set (α i)} (hs : (i : ι), add_salem_spencer (s i)) :
theorem mul_salem_spencer_pi {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), monoid (α i)] {s : Π (i : ι), set (α i)} (hs : (i : ι), mul_salem_spencer (s i)) :
theorem mul_salem_spencer.of_image {F : Type u_1} {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {s : set α} [ α (λ (_x : α), β)] [ β 2] (f : F) (hf : s) (h : mul_salem_spencer (f '' s)) :
theorem add_salem_spencer.of_image {F : Type u_1} {α : Type u_2} {β : Type u_3} {s : set α} [ α (λ (_x : α), β)] [ 2] (f : F) (hf : s) (h : add_salem_spencer (f '' s)) :
theorem mul_salem_spencer.image {F : Type u_1} {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {s : set α} [ β] (f : F) (hf : (s * s)) (h : mul_salem_spencer s) :
theorem add_salem_spencer.image {F : Type u_1} {α : Type u_2} {β : Type u_3} {s : set α} [ β] (f : F) (hf : (s + s)) (h : add_salem_spencer s) :
theorem mul_salem_spencer_insert {α : Type u_2} {s : set α} {a : α} :
( ⦃b c : α⦄, b s c s a * b = c * c a = b) ⦃b c : α⦄, b s c s b * c = a * a b = c
theorem add_salem_spencer_insert {α : Type u_2} {s : set α} {a : α} :
( ⦃b c : α⦄, b s c s a + b = c + c a = b) ⦃b c : α⦄, b s c s b + c = a + a b = c
@[simp]
theorem add_salem_spencer_pair {α : Type u_2} (a b : α) :
@[simp]
theorem mul_salem_spencer_pair {α : Type u_2} (a b : α) :
theorem mul_salem_spencer.mul_left {α : Type u_2} {s : set α} {a : α} (hs : mul_salem_spencer s) :
theorem add_salem_spencer.add_left {α : Type u_2} {s : set α} {a : α} (hs : add_salem_spencer s) :
theorem add_salem_spencer.add_right {α : Type u_2} {s : set α} {a : α} (hs : add_salem_spencer s) :
add_salem_spencer ((λ (_x : α), _x + a) '' s)
theorem mul_salem_spencer.mul_right {α : Type u_2} {s : set α} {a : α} (hs : mul_salem_spencer s) :
mul_salem_spencer ((λ (_x : α), _x * a) '' s)
theorem add_salem_spencer_add_left_iff {α : Type u_2} {s : set α} {a : α} :
theorem mul_salem_spencer_mul_left_iff {α : Type u_2} {s : set α} {a : α} :
theorem add_salem_spencer_add_right_iff {α : Type u_2} {s : set α} {a : α} :
add_salem_spencer ((λ (_x : α), _x + a) '' s)
theorem mul_salem_spencer_mul_right_iff {α : Type u_2} {s : set α} {a : α} :
mul_salem_spencer ((λ (_x : α), _x * a) '' s)
theorem add_salem_spencer_insert_of_lt {α : Type u_2} {s : set α} {a : α} (hs : (i : α), i s i < a) :
⦃b c : α⦄, b s c s a + b = c + c a = b
theorem mul_salem_spencer_insert_of_lt {α : Type u_2} {s : set α} {a : α} (hs : (i : α), i s i < a) :
⦃b c : α⦄, b s c s a * b = c * c a = b
theorem mul_salem_spencer.mul_left₀ {α : Type u_2} {s : set α} {a : α} (hs : mul_salem_spencer s) (ha : a 0) :
theorem mul_salem_spencer.mul_right₀ {α : Type u_2} {s : set α} {a : α} (hs : mul_salem_spencer s) (ha : a 0) :
mul_salem_spencer ((λ (_x : α), _x * a) '' s)
theorem mul_salem_spencer_mul_left_iff₀ {α : Type u_2} {s : set α} {a : α} (ha : a 0) :
theorem mul_salem_spencer_mul_right_iff₀ {α : Type u_2} {s : set α} {a : α} (ha : a 0) :
mul_salem_spencer ((λ (_x : α), _x * a) '' s)
theorem add_salem_spencer_iff_eq_right {s : set } :
⦃a b c : ⦄, a s b s c s a + b = c + c a = c
theorem add_salem_spencer_frontier {𝕜 : Type u_4} {E : Type u_5} [ E] {s : set E} (hs₀ : is_closed s) (hs₁ : s) :

The frontier of a closed strictly convex set only contains trivial arithmetic progressions. The idea is that an arithmetic progression is contained on a line and the frontier of a strictly convex set does not contain lines.

theorem add_salem_spencer_sphere {E : Type u_5} [ E] (x : E) (r : ) :
def add_roth_number {α : Type u_2} [decidable_eq α] [add_monoid α] :

The additive Roth number of a finset is the cardinality of its biggest additive Salem-Spencer subset. The usual Roth number corresponds to add_roth_number (finset.range n), see roth_number_nat.

Equations
def mul_roth_number {α : Type u_2} [decidable_eq α] [monoid α] :

The multiplicative Roth number of a finset is the cardinality of its biggest multiplicative Salem-Spencer subset.

Equations
theorem mul_roth_number_le {α : Type u_2} [decidable_eq α] [monoid α] (s : finset α) :
theorem add_roth_number_le {α : Type u_2} [decidable_eq α] [add_monoid α] (s : finset α) :
theorem mul_roth_number_spec {α : Type u_2} [decidable_eq α] [monoid α] (s : finset α) :
(t : finset α) (H : t s),
theorem add_roth_number_spec {α : Type u_2} [decidable_eq α] [add_monoid α] (s : finset α) :
(t : finset α) (H : t s),
theorem add_salem_spencer.le_add_roth_number {α : Type u_2} [decidable_eq α] [add_monoid α] {s t : finset α} (hs : add_salem_spencer s) (h : s t) :
theorem mul_salem_spencer.le_mul_roth_number {α : Type u_2} [decidable_eq α] [monoid α] {s t : finset α} (hs : mul_salem_spencer s) (h : s t) :
theorem mul_salem_spencer.roth_number_eq {α : Type u_2} [decidable_eq α] [monoid α] {s : finset α} (hs : mul_salem_spencer s) :
@[simp]
theorem add_roth_number_empty {α : Type u_2} [decidable_eq α] [add_monoid α] :
@[simp]
theorem mul_roth_number_empty {α : Type u_2} [decidable_eq α] [monoid α] :
@[simp]
theorem mul_roth_number_singleton {α : Type u_2} [decidable_eq α] [monoid α] (a : α) :
= 1
@[simp]
theorem add_roth_number_singleton {α : Type u_2} [decidable_eq α] [add_monoid α] (a : α) :
= 1
theorem mul_roth_number_union_le {α : Type u_2} [decidable_eq α] [monoid α] (s t : finset α) :
theorem add_roth_number_union_le {α : Type u_2} [decidable_eq α] [add_monoid α] (s t : finset α) :
theorem le_mul_roth_number_product {α : Type u_2} {β : Type u_3} [decidable_eq α] [monoid α] [decidable_eq β] [monoid β] (s : finset α) (t : finset β) :
theorem le_add_roth_number_product {α : Type u_2} {β : Type u_3} [decidable_eq α] [add_monoid α] [decidable_eq β] [add_monoid β] (s : finset α) (t : finset β) :
theorem add_roth_number_lt_of_forall_not_add_salem_spencer {α : Type u_2} [decidable_eq α] [add_monoid α] {s : finset α} {n : } (h : (t : finset α), ) :
theorem mul_roth_number_lt_of_forall_not_mul_salem_spencer {α : Type u_2} [decidable_eq α] [monoid α] {s : finset α} {n : } (h : (t : finset α), ) :
@[simp]
theorem add_roth_number_map_add_left {α : Type u_2} [decidable_eq α] (s : finset α) (a : α) :
@[simp]
theorem mul_roth_number_map_mul_left {α : Type u_2} [decidable_eq α] (s : finset α) (a : α) :
@[simp]
theorem add_roth_number_map_add_right {α : Type u_2} [decidable_eq α] (s : finset α) (a : α) :
@[simp]
theorem mul_roth_number_map_mul_right {α : Type u_2} [decidable_eq α] (s : finset α) (a : α) :
def roth_number_nat  :

The Roth number of a natural N is the largest integer m for which there is a subset of range N of size m with no arithmetic progression of length 3. Trivially, roth_number_nat N ≤ N, but Roth's theorem (proved in 1953) shows that roth_number_nat N = o(N) and the construction by Behrend gives a lower bound of the form N * exp(-C sqrt(log(N))) ≤ roth_number_nat N. A significant refinement of Roth's theorem by Bloom and Sisask announced in 2020 gives roth_number_nat N = O(N / (log N)^(1+c)) for an absolute constant c.

Equations
theorem roth_number_nat_def (n : ) :
theorem roth_number_nat_le (N : ) :
theorem roth_number_nat_spec (n : ) :
(t : (H : t ,
theorem add_salem_spencer.le_roth_number_nat {k n : } (s : finset ) (hs : add_salem_spencer s) (hsn : (x : ), x s x < n) (hsk : s.card = k) :

A verbose specialization of add_salem_spencer.le_add_roth_number, sometimes convenient in practice.

The Roth number is a subadditive function. Note that by Fekete's lemma this shows that the limit roth_number_nat N / N exists, but Roth's theorem gives the stronger result that this limit is actually 0.

@[simp]
theorem roth_number_nat_zero  :
theorem add_roth_number_Ico (a b : ) :
theorem roth_number_nat_is_O_with_id  :
(λ (N : ), (roth_number_nat N)) (λ (N : ), N)

The Roth number has the trivial bound roth_number_nat N = O(N).