mathlib documentation

combinatorics.additive.salem_spencer

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

Main declarations #

TODO #

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]

Whether a given finset is Salem-Spencer is decidable.

Equations
@[protected, instance]

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 α} [fun_like F α (λ (_x : α), β)] [freiman_hom_class F s β 2] (f : F) (hf : set.inj_on f s) (h : mul_salem_spencer (f '' s)) :
theorem add_salem_spencer.of_image {F : Type u_1} {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [add_comm_monoid β] {s : set α} [fun_like F α (λ (_x : α), β)] [add_freiman_hom_class F s β 2] (f : F) (hf : set.inj_on f 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 α} [mul_hom_class F α β] (f : F) (hf : set.inj_on f (s * s)) (h : mul_salem_spencer s) :
theorem add_salem_spencer.image {F : Type u_1} {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [add_comm_monoid β] {s : set α} [add_hom_class F α β] (f : F) (hf : set.inj_on f (s + s)) (h : add_salem_spencer s) :
theorem mul_salem_spencer_insert {α : Type u_2} [cancel_comm_monoid α] {s : set α} {a : α} :
mul_salem_spencer (has_insert.insert a s) mul_salem_spencer s (∀ ⦃b c : α⦄, b sc sa * b = c * ca = b) ∀ ⦃b c : α⦄, b sc sb * c = a * ab = c
theorem add_salem_spencer_insert {α : Type u_2} [add_cancel_comm_monoid α] {s : set α} {a : α} :
add_salem_spencer (has_insert.insert a s) add_salem_spencer s (∀ ⦃b c : α⦄, b sc sa + b = c + ca = b) ∀ ⦃b c : α⦄, b sc sb + c = a + ab = c
@[simp]
theorem add_salem_spencer_pair {α : Type u_2} [add_cancel_comm_monoid α] (a b : α) :
@[simp]
theorem mul_salem_spencer_pair {α : Type u_2} [cancel_comm_monoid α] (a b : α) :
theorem mul_salem_spencer.mul_left {α : Type u_2} [cancel_comm_monoid α] {s : set α} {a : α} (hs : mul_salem_spencer s) :
theorem add_salem_spencer.add_left {α : Type u_2} [add_cancel_comm_monoid α] {s : set α} {a : α} (hs : add_salem_spencer s) :
theorem add_salem_spencer.add_right {α : Type u_2} [add_cancel_comm_monoid α] {s : set α} {a : α} (hs : add_salem_spencer s) :
add_salem_spencer ((λ (_x : α), _x + a) '' s)
theorem mul_salem_spencer.mul_right {α : Type u_2} [cancel_comm_monoid α] {s : set α} {a : α} (hs : mul_salem_spencer s) :
mul_salem_spencer ((λ (_x : α), _x * a) '' s)
theorem add_salem_spencer_add_right_iff {α : Type u_2} [add_cancel_comm_monoid α] {s : set α} {a : α} :
add_salem_spencer ((λ (_x : α), _x + a) '' s) add_salem_spencer s
theorem mul_salem_spencer_mul_right_iff {α : Type u_2} [cancel_comm_monoid α] {s : set α} {a : α} :
mul_salem_spencer ((λ (_x : α), _x * a) '' s) mul_salem_spencer s
theorem add_salem_spencer_insert_of_lt {α : Type u_2} [ordered_cancel_add_comm_monoid α] {s : set α} {a : α} (hs : ∀ (i : α), i si < a) :
add_salem_spencer (has_insert.insert a s) add_salem_spencer s ∀ ⦃b c : α⦄, b sc sa + b = c + ca = b
theorem mul_salem_spencer_insert_of_lt {α : Type u_2} [ordered_cancel_comm_monoid α] {s : set α} {a : α} (hs : ∀ (i : α), i si < a) :
mul_salem_spencer (has_insert.insert a s) mul_salem_spencer s ∀ ⦃b c : α⦄, b sc sa * b = c * ca = b
theorem mul_salem_spencer.mul_left₀ {α : Type u_2} [cancel_comm_monoid_with_zero α] [no_zero_divisors α] {s : set α} {a : α} (hs : mul_salem_spencer s) (ha : a 0) :
theorem mul_salem_spencer.mul_right₀ {α : Type u_2} [cancel_comm_monoid_with_zero α] [no_zero_divisors α] {s : set α} {a : α} (hs : mul_salem_spencer s) (ha : a 0) :
mul_salem_spencer ((λ (_x : α), _x * a) '' s)
theorem mul_salem_spencer_mul_right_iff₀ {α : Type u_2} [cancel_comm_monoid_with_zero α] [no_zero_divisors α] {s : set α} {a : α} (ha : a 0) :
mul_salem_spencer ((λ (_x : α), _x * a) '' s) mul_salem_spencer s
theorem add_salem_spencer_iff_eq_right {s : set } :
add_salem_spencer s ∀ ⦃a b c : ⦄, a sb sc sa + b = c + ca = c
theorem add_salem_spencer_frontier {𝕜 : Type u_4} {E : Type u_5} [linear_ordered_field 𝕜] [topological_space E] [add_comm_monoid E] [module 𝕜 E] {s : set E} (hs₀ : is_closed s) (hs₁ : strict_convex 𝕜 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.

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 α) :
theorem add_roth_number_spec {α : Type u_2} [decidable_eq α] [add_monoid α] (s : finset α) :
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) :
@[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 : α) :
@[simp]
theorem add_roth_number_singleton {α : Type u_2} [decidable_eq α] [add_monoid α] (a : α) :
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 β) :

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 add_salem_spencer.le_roth_number_nat {k n : } (s : finset ) (hs : add_salem_spencer s) (hsn : ∀ (x : ), x sx < 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.

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