Sets without arithmetic progressions of length three and Roth numbers

This file defines sets without arithmetic progressions of length three, aka 3AP-free sets, and the Roth number of a set.

The corresponding notion, sets without geometric progressions of length three, are called 3GP-free sets.

The Roth number of a finset is the size of its biggest 3AP-free 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 3AP-free subset of {0, ..., n - 1}.

Main declarations

• ThreeGPFree: Predicate for a set to be 3GP-free.
• ThreeAPFree: Predicate for a set to be 3AP-free.
• mulRothNumber: The multiplicative Roth number of a finset.
• addRothNumber: The additive Roth number of a finset.
• rothNumberNat: The Roth number of a natural, namely addRothNumber (Finset.range n).

TODO

• Can threeAPFree_iff_eq_right be made more general?
• Generalize ThreeGPFree.image to Freiman homs

References

• Wikipedia, Salem-Spencer set

Tags

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

def ThreeGPFree {α : Type u_2} [Monoid α] (s : Set α) : Prop

A set is 3GP-free if it does not contain any non-trivial geometric progression of length three.

Equations

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

def ThreeAPFree {α : Type u_2} [AddMonoid α] (s : Set α) : Prop

A set is 3AP-free if it does not contain any non-trivial arithmetic progression of length three.

This is also sometimes called a non averaging set or Salem-Spencer set.

Equations

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

instance ThreeGPFree.instDecidable {α : Type u_2} [Monoid α] [DecidableEq α] {s : Finset α} : Decidable (ThreeGPFree ↑s)

Whether a given finset is 3GP-free is decidable.

Equations

• ThreeGPFree.instDecidable = decidable_of_iff (∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, a * c = b * b → a = b) ⋯

instance ThreeAPFree.instDecidable {α : Type u_2} [AddMonoid α] [DecidableEq α] {s : Finset α} : Decidable (ThreeAPFree ↑s)

Whether a given finset is 3AP-free is decidable.

Equations

• ThreeAPFree.instDecidable = decidable_of_iff (∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, a + c = b + b → a = b) ⋯

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

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

@[simp]

theorem threeGPFree_empty {α : Type u_2} [Monoid α] : ThreeGPFree ∅

@[simp]

theorem threeAPFree_empty {α : Type u_2} [AddMonoid α] : ThreeAPFree ∅

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

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

@[simp]

theorem threeGPFree_singleton {α : Type u_2} [Monoid α] (a : α) : ThreeGPFree {a}

@[simp]

theorem threeAPFree_singleton {α : Type u_2} [AddMonoid α] (a : α) : ThreeAPFree {a}

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

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

theorem threeGPFree_pi {ι : Type u_4} {α : ι → Type u_5} [(i : ι) → Monoid (α i)] {s : (i : ι) → Set (α i)} (hs : ∀ (i : ι), ThreeGPFree (s i)) : ThreeGPFree (Set.univ.pi s)

theorem threeAPFree_pi {ι : Type u_4} {α : ι → Type u_5} [(i : ι) → AddMonoid (α i)] {s : (i : ι) → Set (α i)} (hs : ∀ (i : ι), ThreeAPFree (s i)) : ThreeAPFree (Set.univ.pi s)

theorem ThreeGPFree.of_image {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {s : Set α} {A : Set α} {t : Set β} {f : α → β} (hf : IsMulFreimanHom 2 s t f) (hf' : Set.InjOn f s) (hAs : A ⊆ s) (hA : ThreeGPFree (f '' A)) : ThreeGPFree A

Geometric progressions of length three are reflected under 2-Freiman homomorphisms.

theorem ThreeAPFree.of_image {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {s : Set α} {A : Set α} {t : Set β} {f : α → β} (hf : IsAddFreimanHom 2 s t f) (hf' : Set.InjOn f s) (hAs : A ⊆ s) (hA : ThreeAPFree (f '' A)) : ThreeAPFree A

Arithmetic progressions of length three are reflected under 2-Freiman homomorphisms.

theorem threeGPFree_image {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {s : Set α} {A : Set α} {t : Set β} {f : α → β} (hf : IsMulFreimanIso 2 s t f) (hAs : A ⊆ s) : ThreeGPFree (f '' A) ↔ ThreeGPFree A

Geometric progressions of length three are unchanged under 2-Freiman isomorphisms.

theorem threeAPFree_image {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {s : Set α} {A : Set α} {t : Set β} {f : α → β} (hf : IsAddFreimanIso 2 s t f) (hAs : A ⊆ s) : ThreeAPFree (f '' A) ↔ ThreeAPFree A

Arithmetic progressions of length three are unchanged under 2-Freiman isomorphisms.

theorem ThreeGPFree.image {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {s : Set α} {A : Set α} {t : Set β} {f : α → β} (hf : IsMulFreimanIso 2 s t f) (hAs : A ⊆ s) : ThreeGPFree A → ThreeGPFree (f '' A)

Alias of the reverse direction of threeGPFree_image.

---

Geometric progressions of length three are unchanged under 2-Freiman isomorphisms.

theorem ThreeAPFree.image {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {s : Set α} {A : Set α} {t : Set β} {f : α → β} (hf : IsAddFreimanIso 2 s t f) (hAs : A ⊆ s) : ThreeAPFree A → ThreeAPFree (f '' A)

theorem IsMulFreimanHom.threeGPFree {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {s : Set α} {t : Set β} {f : α → β} (hf : IsMulFreimanHom 2 s t f) (hf' : Set.InjOn f s) (ht : ThreeGPFree t) : ThreeGPFree s

Geometric progressions of length three are reflected under 2-Freiman homomorphisms.

theorem IsAddFreimanHom.threeAPFree {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {s : Set α} {t : Set β} {f : α → β} (hf : IsAddFreimanHom 2 s t f) (hf' : Set.InjOn f s) (ht : ThreeAPFree t) : ThreeAPFree s

Arithmetic progressions of length three are reflected under 2-Freiman homomorphisms.

theorem IsMulFreimanIso.threeGPFree_congr {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {s : Set α} {t : Set β} {f : α → β} (hf : IsMulFreimanIso 2 s t f) : ThreeGPFree s ↔ ThreeGPFree t

Geometric progressions of length three are unchanged under 2-Freiman isomorphisms.

theorem IsAddFreimanIso.threeAPFree_congr {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {s : Set α} {t : Set β} {f : α → β} (hf : IsAddFreimanIso 2 s t f) : ThreeAPFree s ↔ ThreeAPFree t

Arithmetic progressions of length three are unchanged under 2-Freiman isomorphisms.

theorem ThreeGPFree.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 : ThreeGPFree s) : ThreeGPFree (⇑f '' s)

Geometric progressions of length three are preserved under semigroup homomorphisms.

theorem ThreeAPFree.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 : ThreeAPFree s) : ThreeAPFree (⇑f '' s)

Arithmetic progressions of length three are preserved under semigroup homomorphisms.

theorem ThreeGPFree.eq_right {α : Type u_2} [CancelCommMonoid α] {s : Set α} (hs : ThreeGPFree s) ⦃a : α⦄ : a ∈ s → ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → b = c

theorem ThreeAPFree.eq_right {α : Type u_2} [AddCancelCommMonoid α] {s : Set α} (hs : ThreeAPFree s) ⦃a : α⦄ : a ∈ s → ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a + c = b + b → b = c

theorem threeGPFree_insert {α : Type u_2} [CancelCommMonoid α] {s : Set α} {a : α} : ThreeGPFree (insert a s) ↔ ThreeGPFree s ∧ (∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a

theorem threeAPFree_insert {α : Type u_2} [AddCancelCommMonoid α] {s : Set α} {a : α} : ThreeAPFree (insert a s) ↔ ThreeAPFree s ∧ (∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a + c = b + b → a = b) ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b + c = a + a → b = a

theorem ThreeGPFree.smul_set {α : Type u_2} [CancelCommMonoid α] {s : Set α} {a : α} (hs : ThreeGPFree s) : ThreeGPFree (a • s)

theorem ThreeAPFree.vadd_set {α : Type u_2} [AddCancelCommMonoid α] {s : Set α} {a : α} (hs : ThreeAPFree s) : ThreeAPFree (a +ᵥ s)

theorem threeGPFree_smul_set {α : Type u_2} [CancelCommMonoid α] {s : Set α} {a : α} : ThreeGPFree (a • s) ↔ ThreeGPFree s

theorem threeAPFree_vadd_set {α : Type u_2} [AddCancelCommMonoid α] {s : Set α} {a : α} : ThreeAPFree (a +ᵥ s) ↔ ThreeAPFree s

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

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

theorem ThreeGPFree.smul_set₀ {α : Type u_2} [CancelCommMonoidWithZero α] [NoZeroDivisors α] {s : Set α} {a : α} (hs : ThreeGPFree s) (ha : a ≠ 0) : ThreeGPFree (a • s)

theorem threeGPFree_smul_set₀ {α : Type u_2} [CancelCommMonoidWithZero α] [NoZeroDivisors α] {s : Set α} {a : α} (ha : a ≠ 0) : ThreeGPFree (a • s) ↔ ThreeGPFree s

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

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

The multiplicative Roth number of a finset is the cardinality of its biggest 3GP-free subset.

Equations

• mulRothNumber = { toFun := fun (s : Finset α) => Nat.findGreatest (fun (m : ℕ) => ∃ t ⊆ s, t.card = m ∧ ThreeGPFree ↑t) s.card, monotone' := ⋯ }

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

The additive Roth number of a finset is the cardinality of its biggest 3AP-free subset.

The usual Roth number corresponds to addRothNumber (Finset.range n), see rothNumberNat.

Equations

• addRothNumber = { toFun := fun (s : Finset α) => Nat.findGreatest (fun (m : ℕ) => ∃ t ⊆ s, t.card = m ∧ ThreeAPFree ↑t) s.card, monotone' := ⋯ }

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem addRothNumber_union_le {α : Type u_2} [DecidableEq α] [AddMonoid α] (s : Finset α) (t : Finset α) : addRothNumber (s ∪ t) ≤ addRothNumber s + addRothNumber 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 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 mulRothNumber_lt_of_forall_not_threeGPFree {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {n : ℕ} (h : ∀ t ∈ Finset.powersetCard n s, ¬ThreeGPFree ↑t) : mulRothNumber s < n

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

theorem IsMulFreimanHom.mulRothNumber_mono {α : Type u_2} {β : Type u_3} [DecidableEq α] [CommMonoid α] [CommMonoid β] [DecidableEq β] {A : Finset α} {B : Finset β} {f : α → β} (hf : IsMulFreimanHom 2 (↑A) (↑B) f) (hf' : Set.BijOn f ↑A ↑B) : mulRothNumber B ≤ mulRothNumber A

Arithmetic progressions can be pushed forward along bijective 2-Freiman homs.

theorem IsAddFreimanHom.addRothNumber_mono {α : Type u_2} {β : Type u_3} [DecidableEq α] [AddCommMonoid α] [AddCommMonoid β] [DecidableEq β] {A : Finset α} {B : Finset β} {f : α → β} (hf : IsAddFreimanHom 2 (↑A) (↑B) f) (hf' : Set.BijOn f ↑A ↑B) : addRothNumber B ≤ addRothNumber A

Arithmetic progressions can be pushed forward along bijective 2-Freiman homs.

theorem IsMulFreimanIso.mulRothNumber_congr {α : Type u_2} {β : Type u_3} [DecidableEq α] [CommMonoid α] [CommMonoid β] [DecidableEq β] {A : Finset α} {B : Finset β} {f : α → β} (hf : IsMulFreimanIso 2 (↑A) (↑B) f) : mulRothNumber A = mulRothNumber B

Arithmetic progressions are preserved under 2-Freiman isos.

theorem IsAddFreimanIso.addRothNumber_congr {α : Type u_2} {β : Type u_3} [DecidableEq α] [AddCommMonoid α] [AddCommMonoid β] [DecidableEq β] {A : Finset α} {B : Finset β} {f : α → β} (hf : IsAddFreimanIso 2 (↑A) (↑B) f) : addRothNumber A = addRothNumber B

Arithmetic progressions are preserved under 2-Freiman isos.

@[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_left {α : Type u_2} [DecidableEq α] [AddCancelCommMonoid α] (s : Finset α) (a : α) : addRothNumber (Finset.map (addLeftEmbedding 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

@[simp]

theorem addRothNumber_map_add_right {α : Type u_2} [DecidableEq α] [AddCancelCommMonoid α] (s : Finset α) (a : α) : addRothNumber (Finset.map (addRightEmbedding a) s) = addRothNumber 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.range n, t.card = rothNumberNat n ∧ ThreeAPFree ↑t

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

A verbose specialization of threeAPFree.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 Fin.addRothNumber_eq_rothNumberNat {k : ℕ} {n : ℕ} (hkn : 2 * k ≤ n) : addRothNumber (Finset.Iio ↑k) = rothNumberNat k

theorem Fin.addRothNumber_le_rothNumberNat (k : ℕ) (n : ℕ) (hkn : k ≤ n) : addRothNumber (Finset.Iio ↑k) ≤ rothNumberNat k