# Salem-Spencer sets and Roth numbers #

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 literature, where the n-th Roth number is the size of the biggest Salem-Spencer subset of {0, ..., n - 1}.

## Main declarations #

• MulSalemSpencer: Predicate for a set to be multiplicative Salem-Spencer.
• AddSalemSpencer: Predicate for a set to be additive Salem-Spencer.
• mulRothNumber: The multiplicative Roth number of a finset.
• addRothNumber: The additive Roth number of a finset.
• rothNumberNat: The Roth number of a natural. This corresponds to addRothNumber (Finset.range n).

## TODO #

• Can addSalemSpencer_iff_eq_right be made more general?
• Generalize MulSalemSpencer.image to Freiman homs

## Tags #

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

def AddSalemSpencer {α : Type u_2} [] (s : Set α) :

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.

Instances For
def MulSalemSpencer {α : Type u_2} [] (s : Set α) :

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.

Instances For
theorem instDecidableAddSalemSpencerToSet.proof_1 {α : Type u_1} [] {s : } :
(∀ (a : α), a s∀ (b : α), b s∀ (c : α), c sa + b = c + ca = b)
instance instDecidableAddSalemSpencerToSet {α : Type u_6} [] [] {s : } :

Whether a given finset is Salem-Spencer is decidable.

instance instDecidableMulSalemSpencerToSet {α : Type u_6} [] [] {s : } :

Whether a given finset is Salem-Spencer is decidable.

theorem AddSalemSpencer.mono {α : Type u_2} [] {s : Set α} {t : Set α} (h : t s) (hs : ) :
theorem MulSalemSpencer.mono {α : Type u_2} [] {s : Set α} {t : Set α} (h : t s) (hs : ) :
@[simp]
theorem addSalemSpencer_empty {α : Type u_2} [] :
@[simp]
theorem mulSalemSpencer_empty {α : Type u_2} [] :
theorem Set.Subsingleton.addSalemSpencer {α : Type u_2} [] {s : Set α} (hs : ) :
theorem Set.Subsingleton.mulSalemSpencer {α : Type u_2} [] {s : Set α} (hs : ) :
@[simp]
theorem addSalemSpencer_singleton {α : Type u_2} [] (a : α) :
@[simp]
theorem mulSalemSpencer_singleton {α : Type u_2} [] (a : α) :
theorem AddSalemSpencer.prod {α : Type u_2} {β : Type u_3} [] [] {s : Set α} {t : Set β} (hs : ) (ht : ) :
theorem MulSalemSpencer.prod {α : Type u_2} {β : Type u_3} [] [] {s : Set α} {t : Set β} (hs : ) (ht : ) :
theorem addSalemSpencer_pi {ι : Type u_6} {α : ιType u_7} [(i : ι) → AddMonoid (α i)] {s : (i : ι) → Set (α i)} (hs : ∀ (i : ι), AddSalemSpencer (s i)) :
theorem mulSalemSpencer_pi {ι : Type u_6} {α : ιType u_7} [(i : ι) → Monoid (α i)] {s : (i : ι) → Set (α i)} (hs : ∀ (i : ι), MulSalemSpencer (s i)) :
MulSalemSpencer (Set.pi Set.univ s)
theorem AddSalemSpencer.of_image {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set α} [FunLike F α fun x => β] [] (f : F) (hf : Set.InjOn (f) s) (h : AddSalemSpencer (f '' s)) :
theorem MulSalemSpencer.of_image {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set α} [FunLike F α fun x => β] [FreimanHomClass F s β 2] (f : F) (hf : Set.InjOn (f) s) (h : MulSalemSpencer (f '' s)) :
theorem AddSalemSpencer.image {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set α} [AddHomClass F α β] (f : F) (hf : Set.InjOn (f) (s + s)) (h : ) :
theorem MulSalemSpencer.image {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] {s : Set α} [MulHomClass F α β] (f : F) (hf : Set.InjOn (f) (s * s)) (h : ) :
theorem addSalemSpencer_insert {α : Type u_2} {s : Set α} {a : α} :
AddSalemSpencer (insert a s) (∀ ⦃b c : α⦄, b sc sa + b = c + ca = b) ∀ ⦃b c : α⦄, b sc sb + c = a + ab = c
theorem mulSalemSpencer_insert {α : Type u_2} [] {s : Set α} {a : α} :
MulSalemSpencer (insert a s) (∀ ⦃b c : α⦄, b sc sa * b = c * ca = b) ∀ ⦃b c : α⦄, b sc sb * c = a * ab = c
@[simp]
theorem addSalemSpencer_pair {α : Type u_2} (a : α) (b : α) :
@[simp]
theorem mulSalemSpencer_pair {α : Type u_2} [] (a : α) (b : α) :
theorem AddSalemSpencer.add_left {α : Type u_2} {s : Set α} {a : α} (hs : ) :
AddSalemSpencer ((fun x x_1 => x + x_1) a '' s)
theorem MulSalemSpencer.mul_left {α : Type u_2} [] {s : Set α} {a : α} (hs : ) :
MulSalemSpencer ((fun x x_1 => x * x_1) a '' s)
theorem AddSalemSpencer.add_right {α : Type u_2} {s : Set α} {a : α} (hs : ) :
AddSalemSpencer ((fun x => x + a) '' s)
theorem MulSalemSpencer.mul_right {α : Type u_2} [] {s : Set α} {a : α} (hs : ) :
MulSalemSpencer ((fun x => x * a) '' s)
theorem addSalemSpencer_add_left_iff {α : Type u_2} {s : Set α} {a : α} :
AddSalemSpencer ((fun x x_1 => x + x_1) a '' s)
theorem mulSalemSpencer_mul_left_iff {α : Type u_2} [] {s : Set α} {a : α} :
MulSalemSpencer ((fun x x_1 => x * x_1) a '' s)
theorem addSalemSpencer_add_right_iff {α : Type u_2} {s : Set α} {a : α} :
AddSalemSpencer ((fun x => x + a) '' s)
theorem mulSalemSpencer_mul_right_iff {α : Type u_2} [] {s : Set α} {a : α} :
MulSalemSpencer ((fun x => x * a) '' s)
theorem addSalemSpencer_insert_of_lt {α : Type u_2} {s : Set α} {a : α} (hs : ∀ (i : α), i si < a) :
AddSalemSpencer (insert a s) ∀ ⦃b c : α⦄, b sc sa + b = c + ca = b
theorem mulSalemSpencer_insert_of_lt {α : Type u_2} {s : Set α} {a : α} (hs : ∀ (i : α), i si < a) :
MulSalemSpencer (insert a s) ∀ ⦃b c : α⦄, b sc sa * b = c * ca = b
theorem MulSalemSpencer.mul_left₀ {α : Type u_2} [] {s : Set α} {a : α} (hs : ) (ha : a 0) :
MulSalemSpencer ((fun x x_1 => x * x_1) a '' s)
theorem MulSalemSpencer.mul_right₀ {α : Type u_2} [] {s : Set α} {a : α} (hs : ) (ha : a 0) :
MulSalemSpencer ((fun x => x * a) '' s)
theorem mulSalemSpencer_mul_left_iff₀ {α : Type u_2} [] {s : Set α} {a : α} (ha : a 0) :
MulSalemSpencer ((fun x x_1 => x * x_1) a '' s)
theorem mulSalemSpencer_mul_right_iff₀ {α : Type u_2} [] {s : Set α} {a : α} (ha : a 0) :
MulSalemSpencer ((fun x => x * a) '' s)
theorem addSalemSpencer_iff_eq_right {s : } :
∀ ⦃a b c : ⦄, a sb sc sa + b = c + ca = c
theorem addSalemSpencer_frontier {𝕜 : Type u_4} {E : Type u_5} [] [] [Module 𝕜 E] {s : Set E} (hs₀ : ) (hs₁ : ) :

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 addSalemSpencer_sphere {E : Type u_5} [] [] (x : E) (r : ) :
def addRothNumber {α : Type u_2} [] [] :

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

Instances For
theorem addRothNumber.proof_1 {α : Type u_1} [] [] ⦃t : ⦃u : (htu : t u) :
Nat.findGreatest (fun m => t x, = m ) () Nat.findGreatest (fun m => t x, = m ) ()
def mulRothNumber {α : Type u_2} [] [] :

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

Instances For
theorem addRothNumber_le {α : Type u_2} [] [] (s : ) :
theorem mulRothNumber_le {α : Type u_2} [] [] (s : ) :
mulRothNumber s
theorem addRothNumber_spec {α : Type u_2} [] [] (s : ) :
theorem mulRothNumber_spec {α : Type u_2} [] [] (s : ) :
t x, = mulRothNumber s
theorem AddSalemSpencer.le_addRothNumber {α : Type u_2} [] [] {s : } {t : } (hs : ) (h : s t) :
theorem MulSalemSpencer.le_mulRothNumber {α : Type u_2} [] [] {s : } {t : } (hs : ) (h : s t) :
mulRothNumber t
theorem AddSalemSpencer.roth_number_eq {α : Type u_2} [] [] {s : } (hs : ) :
theorem MulSalemSpencer.roth_number_eq {α : Type u_2} [] [] {s : } (hs : ) :
mulRothNumber s =
@[simp]
theorem addRothNumber_empty {α : Type u_2} [] [] :
@[simp]
theorem mulRothNumber_empty {α : Type u_2} [] [] :
mulRothNumber = 0
@[simp]
theorem addRothNumber_singleton {α : Type u_2} [] [] (a : α) :
@[simp]
theorem mulRothNumber_singleton {α : Type u_2} [] [] (a : α) :
mulRothNumber {a} = 1
abbrev addRothNumber_union_le.match_1 {α : Type u_1} [] [] (s : ) (t : ) (motive : (t x, = addRothNumber (s t) ) → Prop) :
(x : t x, = addRothNumber (s t) ) → ((u : ) → (hus : u s t) → (hcard : = addRothNumber (s t)) → (hu : ) → motive (_ : t x, = addRothNumber (s t) )) → motive x
Instances For
theorem addRothNumber_union_le {α : Type u_2} [] [] (s : ) (t : ) :
theorem mulRothNumber_union_le {α : Type u_2} [] [] (s : ) (t : ) :
mulRothNumber (s t) mulRothNumber s + mulRothNumber t
theorem le_addRothNumber_product {α : Type u_2} {β : Type u_3} [] [] [] [] (s : ) (t : ) :
theorem le_mulRothNumber_product {α : Type u_2} {β : Type u_3} [] [] [] [] (s : ) (t : ) :
mulRothNumber s * mulRothNumber t mulRothNumber (s ×ˢ t)
theorem addRothNumber_lt_of_forall_not_addSalemSpencer {α : Type u_2} [] [] {s : } {n : } (h : ∀ (t : ), t ) :
theorem mulRothNumber_lt_of_forall_not_mulSalemSpencer {α : Type u_2} [] [] {s : } {n : } (h : ∀ (t : ), t ) :
mulRothNumber s < n
@[simp]
theorem addRothNumber_map_add_left {α : Type u_2} [] (s : ) (a : α) :
@[simp]
theorem mulRothNumber_map_mul_left {α : Type u_2} [] [] (s : ) (a : α) :
mulRothNumber () = mulRothNumber s
@[simp]
theorem addRothNumber_map_add_right {α : Type u_2} [] (s : ) (a : α) :
@[simp]
theorem mulRothNumber_map_mul_right {α : Type u_2} [] [] (s : ) (a : α) :
mulRothNumber () = mulRothNumber s

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, rothNumberNat N ≤ N, but Roth's theorem (proved in 1953) shows that rothNumberNat N = o(N) and the construction by Behrend gives a lower bound of the form N * exp(-C sqrt(log(N))) ≤ rothNumberNat N. A significant refinement of Roth's theorem by Bloom and Sisask announced in 2020 gives rothNumberNat N = O(N / (log N)^(1+c)) for an absolute constant c.

Instances For
theorem rothNumberNat_def (n : ) :
theorem rothNumberNat_le (N : ) :
N
theorem rothNumberNat_spec (n : ) :
t x,
theorem AddSalemSpencer.le_rothNumberNat {k : } {n : } (s : ) (hs : ) (hsn : ∀ (x : ), x sx < n) (hsk : = k) :
k

A verbose specialization of addSalemSpencer.le_addRothNumber, sometimes convenient in practice.

theorem rothNumberNat_add_le (M : ) (N : ) :
rothNumberNat (M + N)

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

@[simp]
theorem rothNumberNat_zero :
= 0
theorem addRothNumber_Ico (a : ) (b : ) :
addRothNumber () = rothNumberNat (b - a)
theorem rothNumberNat_isBigOWith_id :
Asymptotics.IsBigOWith 1 Filter.atTop (fun N => ↑()) fun N => N
theorem rothNumberNat_isBigO_id :
(fun N => ↑()) =O[Filter.atTop] fun N => N

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