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} [AddMonoid α] (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

• AddSalemSpencer s = ∀ ⦃a b c : α⦄, a ∈ s → b ∈ s → c ∈ s → a + b = c + c → a = b

def MulSalemSpencer {α : 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

• MulSalemSpencer s = ∀ ⦃a b c : α⦄, a ∈ s → b ∈ s → c ∈ s → a * b = c * c → a = b

theorem instDecidableAddSalemSpencerToSet.proof_1 {α : Type u_1} [AddMonoid α] {s : Finset α} : (∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, a + b = c + c → a = b) ↔ AddSalemSpencer ↑s

instance instDecidableAddSalemSpencerToSet {α : Type u_6} [DecidableEq α] [AddMonoid α] {s : Finset α} : Decidable (AddSalemSpencer ↑s)

Whether a given finset is Salem-Spencer is decidable.

Equations

• instDecidableAddSalemSpencerToSet = decidable_of_iff (∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, a + b = c + c → a = b) (_ : (∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, a + b = c + c → a = b) ↔ AddSalemSpencer ↑s)

instance instDecidableMulSalemSpencerToSet {α : Type u_6} [DecidableEq α] [Monoid α] {s : Finset α} : Decidable (MulSalemSpencer ↑s)

Whether a given finset is Salem-Spencer is decidable.

Equations

• instDecidableMulSalemSpencerToSet = decidable_of_iff (∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, a * b = c * c → a = b) (_ : (∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, a * b = c * c → a = b) ↔ MulSalemSpencer ↑s)

theorem AddSalemSpencer.mono {α : Type u_2} [AddMonoid α] {s : Set α} {t : Set α} (h : t ⊆ s) (hs : AddSalemSpencer s) : AddSalemSpencer t

theorem MulSalemSpencer.mono {α : Type u_2} [Monoid α] {s : Set α} {t : Set α} (h : t ⊆ s) (hs : MulSalemSpencer s) : MulSalemSpencer t

@[simp]

theorem addSalemSpencer_empty {α : Type u_2} [AddMonoid α] : AddSalemSpencer ∅

@[simp]

theorem mulSalemSpencer_empty {α : Type u_2} [Monoid α] : MulSalemSpencer ∅

theorem Set.Subsingleton.addSalemSpencer {α : Type u_2} [AddMonoid α] {s : Set α} (hs : Set.Subsingleton s) : AddSalemSpencer s

theorem Set.Subsingleton.mulSalemSpencer {α : Type u_2} [Monoid α] {s : Set α} (hs : Set.Subsingleton s) : MulSalemSpencer s

@[simp]

theorem addSalemSpencer_singleton {α : Type u_2} [AddMonoid α] (a : α) : AddSalemSpencer {a}

@[simp]

theorem mulSalemSpencer_singleton {α : Type u_2} [Monoid α] (a : α) : MulSalemSpencer {a}

theorem AddSalemSpencer.prod {α : Type u_2} {β : Type u_3} [AddMonoid α] [AddMonoid β] {s : Set α} {t : Set β} (hs : AddSalemSpencer s) (ht : AddSalemSpencer t) : AddSalemSpencer (s ×ˢ t)

theorem MulSalemSpencer.prod {α : Type u_2} {β : Type u_3} [Monoid α] [Monoid β] {s : Set α} {t : Set β} (hs : MulSalemSpencer s) (ht : MulSalemSpencer t) : MulSalemSpencer (s ×ˢ t)

theorem addSalemSpencer_pi {ι : Type u_6} {α : ι → Type u_7} [(i : ι) → AddMonoid (α i)] {s : (i : ι) → Set (α i)} (hs : ∀ (i : ι), AddSalemSpencer (s i)) : AddSalemSpencer (Set.pi Set.univ s)

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} [AddCommMonoid α] [AddCommMonoid β] {s : Set α} [FunLike F α β] [AddFreimanHomClass F s β 2] (f : F) (hf : Set.InjOn (⇑f) s) (h : AddSalemSpencer (⇑f '' s)) : AddSalemSpencer s

theorem MulSalemSpencer.of_image {F : Type u_1} {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {s : Set α} [FunLike F α β] [FreimanHomClass F s β 2] (f : F) (hf : Set.InjOn (⇑f) s) (h : MulSalemSpencer (⇑f '' s)) : MulSalemSpencer s

theorem AddSalemSpencer.image {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {s : Set α} [FunLike F α β] [AddHomClass F α β] (f : F) (hf : Set.InjOn (⇑f) (s + s)) (h : AddSalemSpencer s) : AddSalemSpencer (⇑f '' s)

theorem MulSalemSpencer.image {F : Type u_1} {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {s : Set α} [FunLike F α β] [MulHomClass F α β] (f : F) (hf : Set.InjOn (⇑f) (s * s)) (h : MulSalemSpencer s) : MulSalemSpencer (⇑f '' s)

theorem addSalemSpencer_insert {α : Type u_2} [AddCancelCommMonoid α] {s : Set α} {a : α} : AddSalemSpencer (insert a s) ↔ AddSalemSpencer s ∧ (∀ ⦃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 mulSalemSpencer_insert {α : Type u_2} [CancelCommMonoid α] {s : Set α} {a : α} : MulSalemSpencer (insert a s) ↔ MulSalemSpencer s ∧ (∀ ⦃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 addSalemSpencer_pair {α : Type u_2} [AddCancelCommMonoid α] (a : α) (b : α) : AddSalemSpencer {a, b}

@[simp]

theorem mulSalemSpencer_pair {α : Type u_2} [CancelCommMonoid α] (a : α) (b : α) : MulSalemSpencer {a, b}

theorem AddSalemSpencer.add_left {α : Type u_2} [AddCancelCommMonoid α] {s : Set α} {a : α} (hs : AddSalemSpencer s) : AddSalemSpencer ((fun (x : α) => a + x) '' s)

theorem MulSalemSpencer.mul_left {α : Type u_2} [CancelCommMonoid α] {s : Set α} {a : α} (hs : MulSalemSpencer s) : MulSalemSpencer ((fun (x : α) => a * x) '' s)

theorem AddSalemSpencer.add_right {α : Type u_2} [AddCancelCommMonoid α] {s : Set α} {a : α} (hs : AddSalemSpencer s) : AddSalemSpencer ((fun (x : α) => x + a) '' s)

theorem MulSalemSpencer.mul_right {α : Type u_2} [CancelCommMonoid α] {s : Set α} {a : α} (hs : MulSalemSpencer s) : MulSalemSpencer ((fun (x : α) => x * a) '' s)

theorem addSalemSpencer_add_left_iff {α : Type u_2} [AddCancelCommMonoid α] {s : Set α} {a : α} : AddSalemSpencer ((fun (x : α) => a + x) '' s) ↔ AddSalemSpencer s

theorem mulSalemSpencer_mul_left_iff {α : Type u_2} [CancelCommMonoid α] {s : Set α} {a : α} : MulSalemSpencer ((fun (x : α) => a * x) '' s) ↔ MulSalemSpencer s

theorem addSalemSpencer_add_right_iff {α : Type u_2} [AddCancelCommMonoid α] {s : Set α} {a : α} : AddSalemSpencer ((fun (x : α) => x + a) '' s) ↔ AddSalemSpencer s

theorem mulSalemSpencer_mul_right_iff {α : Type u_2} [CancelCommMonoid α] {s : Set α} {a : α} : MulSalemSpencer ((fun (x : α) => x * a) '' s) ↔ MulSalemSpencer s

theorem addSalemSpencer_insert_of_lt {α : Type u_2} [OrderedCancelAddCommMonoid α] {s : Set α} {a : α} (hs : ∀ i ∈ s, i < a) : AddSalemSpencer (insert a s) ↔ AddSalemSpencer s ∧ ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → a + b = c + c → a = b

theorem mulSalemSpencer_insert_of_lt {α : Type u_2} [OrderedCancelCommMonoid α] {s : Set α} {a : α} (hs : ∀ i ∈ s, i < a) : MulSalemSpencer (insert a s) ↔ MulSalemSpencer s ∧ ∀ ⦃b c : α⦄, b ∈ s → c ∈ s → a * b = c * c → a = b

theorem MulSalemSpencer.mul_left₀ {α : Type u_2} [CancelCommMonoidWithZero α] [NoZeroDivisors α] {s : Set α} {a : α} (hs : MulSalemSpencer s) (ha : a ≠ 0) : MulSalemSpencer ((fun (x : α) => a * x) '' s)

theorem MulSalemSpencer.mul_right₀ {α : Type u_2} [CancelCommMonoidWithZero α] [NoZeroDivisors α] {s : Set α} {a : α} (hs : MulSalemSpencer s) (ha : a ≠ 0) : MulSalemSpencer ((fun (x : α) => x * a) '' s)

theorem mulSalemSpencer_mul_left_iff₀ {α : Type u_2} [CancelCommMonoidWithZero α] [NoZeroDivisors α] {s : Set α} {a : α} (ha : a ≠ 0) : MulSalemSpencer ((fun (x : α) => a * x) '' s) ↔ MulSalemSpencer s

theorem mulSalemSpencer_mul_right_iff₀ {α : Type u_2} [CancelCommMonoidWithZero α] [NoZeroDivisors α] {s : Set α} {a : α} (ha : a ≠ 0) : MulSalemSpencer ((fun (x : α) => x * a) '' s) ↔ MulSalemSpencer s

theorem addSalemSpencer_iff_eq_right {s : Set ℕ} : AddSalemSpencer s ↔ ∀ ⦃a b c : ℕ⦄, a ∈ s → b ∈ s → c ∈ s → a + b = c + c → a = c

theorem addSalemSpencer_frontier {𝕜 : Type u_4} {E : Type u_5} [LinearOrderedField 𝕜] [TopologicalSpace E] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs₀ : IsClosed s) (hs₁ : StrictConvex 𝕜 s) : AddSalemSpencer (frontier 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 addSalemSpencer_sphere {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [StrictConvexSpace ℝ E] (x : E) (r : ℝ) : AddSalemSpencer (Metric.sphere x r)

def addRothNumber {α : Type u_2} [DecidableEq α] [AddMonoid α] : Finset α →o ℕ

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.

Equations

• One or more equations did not get rendered due to their size.

theorem addRothNumber.proof_1 {α : Type u_1} [DecidableEq α] [AddMonoid α] ⦃t : Finset α⦄ ⦃u : Finset α⦄ (htu : t ≤ u) : Nat.findGreatest (fun (m : ℕ) => ∃ (t_1 : Finset α) (_ : t_1 ⊆ t), t_1.card = m ∧ AddSalemSpencer ↑t_1) t.card ≤ Nat.findGreatest (fun (m : ℕ) => ∃ (t : Finset α) (_ : t ⊆ u), t.card = m ∧ AddSalemSpencer ↑t) u.card

def mulRothNumber {α : Type u_2} [DecidableEq α] [Monoid α] : Finset α →o ℕ

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

Equations

• One or more equations did not get rendered due to their size.

theorem addRothNumber_le {α : Type u_2} [DecidableEq α] [AddMonoid α] (s : Finset α) : addRothNumber s ≤ s.card

theorem mulRothNumber_le {α : Type u_2} [DecidableEq α] [Monoid α] (s : Finset α) : mulRothNumber s ≤ s.card

theorem addRothNumber_spec {α : Type u_2} [DecidableEq α] [AddMonoid α] (s : Finset α) : ∃ (t : Finset α) (_ : t ⊆ s), t.card = addRothNumber s ∧ AddSalemSpencer ↑t

theorem mulRothNumber_spec {α : Type u_2} [DecidableEq α] [Monoid α] (s : Finset α) : ∃ (t : Finset α) (_ : t ⊆ s), t.card = mulRothNumber s ∧ MulSalemSpencer ↑t

theorem AddSalemSpencer.le_addRothNumber {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} {t : Finset α} (hs : AddSalemSpencer ↑s) (h : s ⊆ t) : s.card ≤ addRothNumber t

theorem MulSalemSpencer.le_mulRothNumber {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {t : Finset α} (hs : MulSalemSpencer ↑s) (h : s ⊆ t) : s.card ≤ mulRothNumber t

theorem AddSalemSpencer.roth_number_eq {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} (hs : AddSalemSpencer ↑s) : addRothNumber s = s.card

theorem MulSalemSpencer.roth_number_eq {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} (hs : MulSalemSpencer ↑s) : mulRothNumber s = s.card

@[simp]

theorem addRothNumber_empty {α : Type u_2} [DecidableEq α] [AddMonoid α] : addRothNumber ∅ = 0

@[simp]

theorem mulRothNumber_empty {α : Type u_2} [DecidableEq α] [Monoid α] : mulRothNumber ∅ = 0

@[simp]

theorem addRothNumber_singleton {α : Type u_2} [DecidableEq α] [AddMonoid α] (a : α) : addRothNumber {a} = 1

@[simp]

theorem mulRothNumber_singleton {α : Type u_2} [DecidableEq α] [Monoid α] (a : α) : mulRothNumber {a} = 1

abbrev addRothNumber_union_le.match_1 {α : Type u_1} [DecidableEq α] [AddMonoid α] (s : Finset α) (t : Finset α) (motive : (∃ (t_1 : Finset α) (_ : t_1 ⊆ s ∪ t), t_1.card = addRothNumber (s ∪ t) ∧ AddSalemSpencer ↑t_1) → Prop) : ∀ (x : ∃ (t_1 : Finset α) (_ : t_1 ⊆ s ∪ t), t_1.card = addRothNumber (s ∪ t) ∧ AddSalemSpencer ↑t_1), (∀ (u : Finset α) (hus : u ⊆ s ∪ t) (hcard : u.card = addRothNumber (s ∪ t)) (hu : AddSalemSpencer ↑u), motive (_ : ∃ (t_1 : Finset α) (_ : t_1 ⊆ s ∪ t), t_1.card = addRothNumber (s ∪ t) ∧ AddSalemSpencer ↑t_1)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

theorem addRothNumber_union_le {α : Type u_2} [DecidableEq α] [AddMonoid α] (s : Finset α) (t : Finset α) : addRothNumber (s ∪ t) ≤ addRothNumber s + addRothNumber t

theorem mulRothNumber_union_le {α : Type u_2} [DecidableEq α] [Monoid α] (s : Finset α) (t : Finset α) : mulRothNumber (s ∪ t) ≤ mulRothNumber s + mulRothNumber t

theorem le_addRothNumber_product {α : Type u_2} {β : Type u_3} [DecidableEq α] [AddMonoid α] [DecidableEq β] [AddMonoid β] (s : Finset α) (t : Finset β) : addRothNumber s * addRothNumber t ≤ addRothNumber (s ×ˢ t)

theorem le_mulRothNumber_product {α : Type u_2} {β : Type u_3} [DecidableEq α] [Monoid α] [DecidableEq β] [Monoid β] (s : Finset α) (t : Finset β) : mulRothNumber s * mulRothNumber t ≤ mulRothNumber (s ×ˢ t)

theorem addRothNumber_lt_of_forall_not_addSalemSpencer {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} {n : ℕ} (h : ∀ t ∈ Finset.powersetCard n s, ¬AddSalemSpencer ↑t) : addRothNumber s < n

theorem mulRothNumber_lt_of_forall_not_mulSalemSpencer {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {n : ℕ} (h : ∀ t ∈ Finset.powersetCard n s, ¬MulSalemSpencer ↑t) : mulRothNumber s < n

@[simp]

theorem addRothNumber_map_add_left {α : Type u_2} [DecidableEq α] [AddCancelCommMonoid α] (s : Finset α) (a : α) : addRothNumber (Finset.map (addLeftEmbedding a) s) = addRothNumber s

@[simp]

theorem mulRothNumber_map_mul_left {α : Type u_2} [DecidableEq α] [CancelCommMonoid α] (s : Finset α) (a : α) : mulRothNumber (Finset.map (mulLeftEmbedding a) s) = mulRothNumber s

@[simp]

theorem addRothNumber_map_add_right {α : Type u_2} [DecidableEq α] [AddCancelCommMonoid α] (s : Finset α) (a : α) : addRothNumber (Finset.map (addRightEmbedding a) s) = addRothNumber s

@[simp]

theorem mulRothNumber_map_mul_right {α : Type u_2} [DecidableEq α] [CancelCommMonoid α] (s : Finset α) (a : α) : mulRothNumber (Finset.map (mulRightEmbedding a) s) = mulRothNumber s

def rothNumberNat : ℕ →o ℕ

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.

Equations

• rothNumberNat = { toFun := fun (n : ℕ) => addRothNumber (Finset.range n), monotone' := rothNumberNat.proof_1 }

theorem rothNumberNat_def (n : ℕ) : rothNumberNat n = addRothNumber (Finset.range n)

theorem rothNumberNat_le (N : ℕ) : rothNumberNat N ≤ N

theorem rothNumberNat_spec (n : ℕ) : ∃ (t : Finset ℕ) (_ : t ⊆ Finset.range n), t.card = rothNumberNat n ∧ AddSalemSpencer ↑t

theorem AddSalemSpencer.le_rothNumberNat {k : ℕ} {n : ℕ} (s : Finset ℕ) (hs : AddSalemSpencer ↑s) (hsn : ∀ x ∈ s, x < n) (hsk : s.card = k) : k ≤ rothNumberNat n

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

theorem rothNumberNat_add_le (M : ℕ) (N : ℕ) : rothNumberNat (M + N) ≤ rothNumberNat M + rothNumberNat 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 : rothNumberNat 0 = 0

theorem addRothNumber_Ico (a : ℕ) (b : ℕ) : addRothNumber (Finset.Ico a b) = rothNumberNat (b - a)

theorem rothNumberNat_isBigOWith_id : Asymptotics.IsBigOWith 1 Filter.atTop (fun (N : ℕ) => ↑(rothNumberNat N)) fun (N : ℕ) => ↑N

theorem rothNumberNat_isBigO_id : (fun (N : ℕ) => ↑(rothNumberNat N)) =O[Filter.atTop] fun (N : ℕ) => ↑N

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