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 #
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 toadd_roth_number (finset.range n).
TODO #
Can add_salem_spencer_iff_eq_right be made more general?
Tags #
Salem-Spencer, Roth, arithmetic progression, average, three-free
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.
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.
@[protected, instance]
Equations
- add_salem_spencer.decidable = decidable_of_iff (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → ∀ (c : α), c ∈ s → a + b = c + c → a = b) add_salem_spencer.decidable._proof_1
@[protected, instance]
Whether a given finset is Salem-Spencer is decidable.
Equations
- mul_salem_spencer.decidable = decidable_of_iff (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → ∀ (c : α), c ∈ s → a * b = c * c → a = b) mul_salem_spencer.decidable._proof_1
theorem
add_salem_spencer.mono
{α : Type u_1}
[add_monoid α]
{s t : set α}
(h : t ⊆ s)
(hs : add_salem_spencer s) :
theorem
mul_salem_spencer.mono
{α : Type u_1}
[monoid α]
{s t : set α}
(h : t ⊆ s)
(hs : mul_salem_spencer s) :
theorem
set.subsingleton.add_salem_spencer
{α : Type u_1}
[add_monoid α]
{s : set α}
(hs : s.subsingleton) :
theorem
set.subsingleton.mul_salem_spencer
{α : Type u_1}
[monoid α]
{s : set α}
(hs : s.subsingleton) :
@[simp]
@[simp]
theorem
add_salem_spencer.sum
{α : Type u_1}
{β : Type u_2}
[add_monoid α]
[add_monoid β]
{s : set α}
{t : set β}
(hs : add_salem_spencer s)
(ht : add_salem_spencer t) :
add_salem_spencer (s ×ˢ t)
theorem
mul_salem_spencer.prod
{α : Type u_1}
{β : Type u_2}
[monoid α]
[monoid β]
{s : set α}
{t : set β}
(hs : mul_salem_spencer s)
(ht : mul_salem_spencer t) :
mul_salem_spencer (s ×ˢ 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)) :
@[simp]
theorem
add_salem_spencer_pair
{α : Type u_1}
[add_cancel_comm_monoid α]
(a b : α) :
add_salem_spencer {a, b}
@[simp]
theorem
mul_salem_spencer_pair
{α : Type u_1}
[cancel_comm_monoid α]
(a b : α) :
mul_salem_spencer {a, b}
theorem
mul_salem_spencer.mul_left
{α : Type u_1}
[cancel_comm_monoid α]
{s : set α}
{a : α}
(hs : mul_salem_spencer s) :
mul_salem_spencer (has_mul.mul a '' s)
theorem
add_salem_spencer.add_left
{α : Type u_1}
[add_cancel_comm_monoid α]
{s : set α}
{a : α}
(hs : add_salem_spencer s) :
add_salem_spencer (has_add.add a '' s)
theorem
add_salem_spencer.add_right
{α : Type u_1}
[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_1}
[cancel_comm_monoid α]
{s : set α}
{a : α}
(hs : mul_salem_spencer s) :
mul_salem_spencer ((λ (_x : α), _x * a) '' s)
theorem
add_salem_spencer_add_left_iff
{α : Type u_1}
[add_cancel_comm_monoid α]
{s : set α}
{a : α} :
add_salem_spencer (has_add.add a '' s) ↔ add_salem_spencer s
theorem
mul_salem_spencer_mul_left_iff
{α : Type u_1}
[cancel_comm_monoid α]
{s : set α}
{a : α} :
mul_salem_spencer (has_mul.mul a '' s) ↔ mul_salem_spencer s
theorem
add_salem_spencer_add_right_iff
{α : Type u_1}
[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_1}
[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_1}
[ordered_cancel_add_comm_monoid α]
{s : set α}
{a : α}
(hs : ∀ (i : α), i ∈ s → i < a) :
theorem
mul_salem_spencer_insert_of_lt
{α : Type u_1}
[ordered_cancel_comm_monoid α]
{s : set α}
{a : α}
(hs : ∀ (i : α), i ∈ s → i < a) :
theorem
mul_salem_spencer.mul_left₀
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[no_zero_divisors α]
{s : set α}
{a : α}
(hs : mul_salem_spencer s)
(ha : a ≠ 0) :
mul_salem_spencer (has_mul.mul a '' s)
theorem
mul_salem_spencer.mul_right₀
{α : Type u_1}
[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_left_iff₀
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[no_zero_divisors α]
{s : set α}
{a : α}
(ha : a ≠ 0) :
mul_salem_spencer (has_mul.mul a '' s) ↔ mul_salem_spencer s
theorem
mul_salem_spencer_mul_right_iff₀
{α : Type u_1}
[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
The additive Roth number of a finset is the cardinality of its biggest additive
Salem-Spencer subset. The usual Roth number corresponds to roth_number (finset.range n), see
roth_number_nat.
The multiplicative Roth number of a finset is the cardinality of its biggest multiplicative Salem-Spencer subset.
theorem
mul_roth_number_le
{α : Type u_1}
[decidable_eq α]
[monoid α]
(s : finset α) :
⇑mul_roth_number s ≤ s.card
theorem
add_roth_number_le
{α : Type u_1}
[decidable_eq α]
[add_monoid α]
(s : finset α) :
⇑add_roth_number s ≤ s.card
theorem
mul_roth_number_spec
{α : Type u_1}
[decidable_eq α]
[monoid α]
(s : finset α) :
∃ (t : finset α) (H : t ⊆ s), t.card = ⇑mul_roth_number s ∧ mul_salem_spencer ↑t
theorem
add_roth_number_spec
{α : Type u_1}
[decidable_eq α]
[add_monoid α]
(s : finset α) :
∃ (t : finset α) (H : t ⊆ s), t.card = ⇑add_roth_number s ∧ add_salem_spencer ↑t
theorem
add_salem_spencer.le_add_roth_number
{α : Type u_1}
[decidable_eq α]
[add_monoid α]
{s t : finset α}
(hs : add_salem_spencer ↑s)
(h : s ⊆ t) :
s.card ≤ ⇑add_roth_number t
theorem
mul_salem_spencer.le_mul_roth_number
{α : Type u_1}
[decidable_eq α]
[monoid α]
{s t : finset α}
(hs : mul_salem_spencer ↑s)
(h : s ⊆ t) :
s.card ≤ ⇑mul_roth_number t
theorem
mul_salem_spencer.roth_number_eq
{α : Type u_1}
[decidable_eq α]
[monoid α]
{s : finset α}
(hs : mul_salem_spencer ↑s) :
⇑mul_roth_number s = s.card
theorem
add_salem_spencer.roth_number_eq
{α : Type u_1}
[decidable_eq α]
[add_monoid α]
{s : finset α}
(hs : add_salem_spencer ↑s) :
⇑add_roth_number s = s.card
@[simp]
@[simp]
@[simp]
theorem
mul_roth_number_singleton
{α : Type u_1}
[decidable_eq α]
[monoid α]
(a : α) :
⇑mul_roth_number {a} = 1
@[simp]
theorem
add_roth_number_singleton
{α : Type u_1}
[decidable_eq α]
[add_monoid α]
(a : α) :
⇑add_roth_number {a} = 1
theorem
mul_roth_number_union_le
{α : Type u_1}
[decidable_eq α]
[monoid α]
(s t : finset α) :
⇑mul_roth_number (s ∪ t) ≤ ⇑mul_roth_number s + ⇑mul_roth_number t
theorem
add_roth_number_union_le
{α : Type u_1}
[decidable_eq α]
[add_monoid α]
(s t : finset α) :
⇑add_roth_number (s ∪ t) ≤ ⇑add_roth_number s + ⇑add_roth_number t
theorem
le_mul_roth_number_product
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
[monoid α]
[decidable_eq β]
[monoid β]
(s : finset α)
(t : finset β) :
(⇑mul_roth_number s) * ⇑mul_roth_number t ≤ ⇑mul_roth_number (s.product t)
theorem
le_add_roth_number_product
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
[add_monoid α]
[decidable_eq β]
[add_monoid β]
(s : finset α)
(t : finset β) :
(⇑add_roth_number s) * ⇑add_roth_number t ≤ ⇑add_roth_number (s.product t)
theorem
add_roth_number_lt_of_forall_not_add_salem_spencer
{α : Type u_1}
[decidable_eq α]
[add_monoid α]
{s : finset α}
{n : ℕ}
(h : ∀ (t : finset α), t ∈ finset.powerset_len n s → ¬add_salem_spencer ↑t) :
⇑add_roth_number s < n
theorem
mul_roth_number_lt_of_forall_not_mul_salem_spencer
{α : Type u_1}
[decidable_eq α]
[monoid α]
{s : finset α}
{n : ℕ}
(h : ∀ (t : finset α), t ∈ finset.powerset_len n s → ¬mul_salem_spencer ↑t) :
⇑mul_roth_number s < n
@[simp]
theorem
add_roth_number_map_add_left
{α : Type u_1}
[decidable_eq α]
[add_cancel_comm_monoid α]
(s : finset α)
(a : α) :
@[simp]
theorem
mul_roth_number_map_mul_left
{α : Type u_1}
[decidable_eq α]
[cancel_comm_monoid α]
(s : finset α)
(a : α) :
@[simp]
theorem
add_roth_number_map_add_right
{α : Type u_1}
[decidable_eq α]
[add_cancel_comm_monoid α]
(s : finset α)
(a : α) :
@[simp]
theorem
mul_roth_number_map_mul_right
{α : Type u_1}
[decidable_eq α]
[cancel_comm_monoid α]
(s : finset α)
(a : α) :
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 N ≤ N, but Roth's theorem (proved in 1953) shows that
roth_number N = o(N) and the construction by Behrend gives a lower bound of the form
N * exp(-C sqrt(log(N))) ≤ roth_number N.
A significant refinement of Roth's theorem by Bloom and Sisask announced in 2020 gives
roth_number N = O(N / (log N)^(1+c)) for an absolute constant c.
Equations
- roth_number_nat = {to_fun := λ (n : ℕ), ⇑add_roth_number (finset.range n), monotone' := roth_number_nat._proof_1}
theorem
roth_number_nat_spec
(n : ℕ) :
∃ (t : finset ℕ) (H : t ⊆ finset.range n), t.card = ⇑roth_number_nat n ∧ add_salem_spencer ↑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) :
k ≤ ⇑roth_number_nat n
A verbose specialization of add_salem_spencer.le_add_roth_number, sometimes convenient in
practice.
theorem
roth_number_nat_add_le
(M N : ℕ) :
⇑roth_number_nat (M + N) ≤ ⇑roth_number_nat M + ⇑roth_number_nat N
The Roth number is a subadditive function. Note that by Fekete's lemma this shows that
the limit roth_number N / N exists, but Roth's theorem gives the stronger result that this
limit is actually 0.
theorem
add_roth_number_Ico
(a b : ℕ) :
⇑add_roth_number (finset.Ico a b) = ⇑roth_number_nat (b - a)
theorem
roth_number_nat_is_O_with_id
:
asymptotics.is_O_with 1 (λ (N : ℕ), ↑(⇑roth_number_nat N)) (λ (N : ℕ), ↑N) filter.at_top
theorem
roth_number_nat_is_O_id
:
asymptotics.is_O (λ (N : ℕ), ↑(⇑roth_number_nat N)) (λ (N : ℕ), ↑N) filter.at_top
The Roth number has the trivial bound roth_number N = O(N).