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 toadd_roth_number (finset.range n).
TODO #
- Can
add_salem_spencer_iff_eq_rightbe made more general? - Generalize
mul_salem_spencer.imageto Freiman homs
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.
Instances for add_salem_spencer
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 mul_salem_spencer
@[protected, instance]
Whether a given finset is Salem-Spencer is decidable.
@[protected, instance]
Whether a given finset is Salem-Spencer is decidable.
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) :
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]
@[simp]
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) :
add_salem_spencer (s ×ˢ 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) :
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)) :
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) :
mul_salem_spencer (⇑f '' 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) :
add_salem_spencer (⇑f '' s)
@[simp]
theorem
add_salem_spencer_pair
{α : Type u_2}
[add_cancel_comm_monoid α]
(a b : α) :
add_salem_spencer {a, b}
@[simp]
theorem
mul_salem_spencer_pair
{α : Type u_2}
[cancel_comm_monoid α]
(a b : α) :
mul_salem_spencer {a, b}
theorem
mul_salem_spencer.mul_left
{α : Type u_2}
[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_2}
[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_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_left_iff
{α : Type u_2}
[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_2}
[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_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 ∈ s → i < a) :
add_salem_spencer (has_insert.insert a s) ↔ add_salem_spencer s ∧ ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → a + b = c + c → a = b
theorem
mul_salem_spencer_insert_of_lt
{α : Type u_2}
[ordered_cancel_comm_monoid α]
{s : set α}
{a : α}
(hs : ∀ (i : α), i ∈ s → i < a) :
mul_salem_spencer (has_insert.insert a s) ↔ mul_salem_spencer s ∧ ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → a * b = c * c → a = 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) :
mul_salem_spencer (has_mul.mul a '' s)
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_left_iff₀
{α : Type u_2}
[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_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_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.
theorem
add_salem_spencer_sphere
{E : Type u_5}
[normed_add_comm_group E]
[normed_space ℝ E]
[strict_convex_space ℝ E]
(x : E)
(r : ℝ) :
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.
The multiplicative Roth number of a finset is the cardinality of its biggest multiplicative Salem-Spencer subset.
theorem
mul_roth_number_le
{α : Type u_2}
[decidable_eq α]
[monoid α]
(s : finset α) :
⇑mul_roth_number s ≤ s.card
theorem
add_roth_number_le
{α : Type u_2}
[decidable_eq α]
[add_monoid α]
(s : finset α) :
⇑add_roth_number s ≤ s.card
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) :
s.card ≤ ⇑add_roth_number 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) :
s.card ≤ ⇑mul_roth_number t
theorem
mul_salem_spencer.roth_number_eq
{α : Type u_2}
[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_2}
[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_2}
[decidable_eq α]
[monoid α]
(a : α) :
⇑mul_roth_number {a} = 1
@[simp]
theorem
add_roth_number_singleton
{α : Type u_2}
[decidable_eq α]
[add_monoid α]
(a : α) :
⇑add_roth_number {a} = 1
theorem
mul_roth_number_union_le
{α : Type u_2}
[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_2}
[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_2}
{β : Type u_3}
[decidable_eq α]
[monoid α]
[decidable_eq β]
[monoid β]
(s : finset α)
(t : finset β) :
⇑mul_roth_number s * ⇑mul_roth_number t ≤ ⇑mul_roth_number (s ×ˢ t)
theorem
le_add_roth_number_product
{α : Type u_2}
{β : Type u_3}
[decidable_eq α]
[add_monoid α]
[decidable_eq β]
[add_monoid β]
(s : finset α)
(t : finset β) :
⇑add_roth_number s * ⇑add_roth_number t ≤ ⇑add_roth_number (s ×ˢ t)
theorem
add_roth_number_lt_of_forall_not_add_salem_spencer
{α : Type u_2}
[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_2}
[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_2}
[decidable_eq α]
[add_cancel_comm_monoid α]
(s : finset α)
(a : α) :
@[simp]
theorem
mul_roth_number_map_mul_left
{α : Type u_2}
[decidable_eq α]
[cancel_comm_monoid α]
(s : finset α)
(a : α) :
@[simp]
theorem
add_roth_number_map_add_right
{α : Type u_2}
[decidable_eq α]
[add_cancel_comm_monoid α]
(s : finset α)
(a : α) :
@[simp]
theorem
mul_roth_number_map_mul_right
{α : Type u_2}
[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_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
- 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_nat 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 filter.at_top (λ (N : ℕ), ↑(⇑roth_number_nat N)) (λ (N : ℕ), ↑N)
theorem
roth_number_nat_is_O_id
:
(λ (N : ℕ), ↑(⇑roth_number_nat N)) =O[filter.at_top] λ (N : ℕ), ↑N
The Roth number has the trivial bound roth_number_nat N = O(N).