Documentation

Mathlib.Combinatorics.Additive.AP.Three.Defs

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 #

TODO #

References #

Tags #

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

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

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 sa + c = b + ba = b
Instances For
    def ThreeGPFree {α : Type u_2} [Monoid α] (s : Set α) :

    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 sa * c = b * ba = b
    Instances For
      theorem ThreeAPFree.instDecidable.proof_1 {α : Type u_1} [AddMonoid α] {s : Finset α} :
      (∀ as, bs, cs, a + c = b + ba = b) as, bs, cs, a + c = b + ba = b
      instance ThreeAPFree.instDecidable {α : Type u_2} [AddMonoid α] [DecidableEq α] {s : Finset α} :

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

      Equations
      • ThreeAPFree.instDecidable = decidable_of_iff (∀ as, bs, cs, a + c = b + ba = b)
      instance ThreeGPFree.instDecidable {α : Type u_2} [Monoid α] [DecidableEq α] {s : Finset α} :

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

      Equations
      • ThreeGPFree.instDecidable = decidable_of_iff (∀ as, bs, cs, a * c = b * ba = b)
      theorem ThreeAPFree.mono {α : Type u_2} [AddMonoid α] {s : Set α} {t : Set α} (h : t s) (hs : ThreeAPFree s) :
      theorem ThreeGPFree.mono {α : Type u_2} [Monoid α] {s : Set α} {t : Set α} (h : t s) (hs : ThreeGPFree s) :
      @[simp]
      @[simp]
      theorem threeGPFree_empty {α : Type u_2} [Monoid α] :
      theorem Set.Subsingleton.threeAPFree {α : Type u_2} [AddMonoid α] {s : Set α} (hs : s.Subsingleton) :
      theorem Set.Subsingleton.threeGPFree {α : Type u_2} [Monoid α] {s : Set α} (hs : s.Subsingleton) :
      @[simp]
      theorem threeAPFree_singleton {α : Type u_2} [AddMonoid α] (a : α) :
      @[simp]
      theorem threeGPFree_singleton {α : Type u_2} [Monoid α] (a : α) :
      theorem ThreeAPFree.prod {α : Type u_2} {β : Type u_3} [AddMonoid α] [AddMonoid β] {s : Set α} {t : Set β} (hs : ThreeAPFree s) (ht : ThreeAPFree t) :
      theorem ThreeGPFree.prod {α : Type u_2} {β : Type u_3} [Monoid α] [Monoid β] {s : Set α} {t : Set β} (hs : ThreeGPFree s) (ht : ThreeGPFree t) :
      theorem threeAPFree_pi {ι : Type u_6} {α : ιType u_7} [(i : ι) → AddMonoid (α i)] {s : (i : ι) → Set (α i)} (hs : ∀ (i : ι), ThreeAPFree (s i)) :
      ThreeAPFree (Set.univ.pi s)
      theorem threeGPFree_pi {ι : Type u_6} {α : ιType u_7} [(i : ι) → Monoid (α i)] {s : (i : ι) → Set (α i)} (hs : ∀ (i : ι), ThreeGPFree (s i)) :
      ThreeGPFree (Set.univ.pi s)
      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)) :

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

      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)) :

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

      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) :

      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) :

      Geometric 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) :

      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) :
      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) :

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

      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) :

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

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

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

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

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

      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.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.eq_right {α : Type u_2} [AddCancelCommMonoid α] {s : Set α} (hs : ThreeAPFree s) ⦃a : α :
      a s∀ ⦃b : α⦄, b s∀ ⦃c : α⦄, c sa + c = b + bb = c
      theorem ThreeGPFree.eq_right {α : Type u_2} [CancelCommMonoid α] {s : Set α} (hs : ThreeGPFree s) ⦃a : α :
      a s∀ ⦃b : α⦄, b s∀ ⦃c : α⦄, c sa * c = b * bb = c
      theorem threeAPFree_insert {α : Type u_2} [AddCancelCommMonoid α] {s : Set α} {a : α} :
      ThreeAPFree (insert a s) ThreeAPFree s (∀ ⦃b : α⦄, b s∀ ⦃c : α⦄, c sa + c = b + ba = b) ∀ ⦃b : α⦄, b s∀ ⦃c : α⦄, c sb + c = a + ab = a
      theorem threeGPFree_insert {α : Type u_2} [CancelCommMonoid α] {s : Set α} {a : α} :
      ThreeGPFree (insert a s) ThreeGPFree s (∀ ⦃b : α⦄, b s∀ ⦃c : α⦄, c sa * c = b * ba = b) ∀ ⦃b : α⦄, b s∀ ⦃c : α⦄, c sb * c = a * ab = a
      theorem ThreeAPFree.vadd_set {α : Type u_2} [AddCancelCommMonoid α] {s : Set α} {a : α} (hs : ThreeAPFree s) :
      theorem ThreeGPFree.smul_set {α : Type u_2} [CancelCommMonoid α] {s : Set α} {a : α} (hs : ThreeGPFree s) :
      theorem threeAPFree_vadd_set {α : Type u_2} [AddCancelCommMonoid α] {s : Set α} {a : α} :
      theorem threeGPFree_smul_set {α : Type u_2} [CancelCommMonoid α] {s : Set α} {a : α} :
      theorem threeAPFree_insert_of_lt {α : Type u_2} [OrderedCancelAddCommMonoid α] {s : Set α} {a : α} (hs : is, i < a) :
      ThreeAPFree (insert a s) ThreeAPFree s ∀ ⦃b : α⦄, b s∀ ⦃c : α⦄, c sa + c = b + ba = b
      theorem threeGPFree_insert_of_lt {α : Type u_2} [OrderedCancelCommMonoid α] {s : Set α} {a : α} (hs : is, i < a) :
      ThreeGPFree (insert a s) ThreeGPFree s ∀ ⦃b : α⦄, b s∀ ⦃c : α⦄, c sa * c = b * ba = b
      theorem ThreeGPFree.smul_set₀ {α : Type u_2} [CancelCommMonoidWithZero α] [NoZeroDivisors α] {s : Set α} {a : α} (hs : ThreeGPFree s) (ha : a 0) :
      theorem threeGPFree_smul_set₀ {α : Type u_2} [CancelCommMonoidWithZero α] [NoZeroDivisors α] {s : Set α} {a : α} (ha : a 0) :
      theorem threeAPFree_iff_eq_right {s : Set } :
      ThreeAPFree s ∀ ⦃a : ⦄, a s∀ ⦃b : ⦄, b s∀ ⦃c : ⦄, c sa + c = b + ba = c
      theorem addRothNumber.proof_1 {α : Type u_1} [DecidableEq α] [AddMonoid α] ⦃t : Finset α ⦃u : Finset α (htu : t u) :
      Nat.findGreatest (fun (m : ) => t_1t, t_1.card = m ThreeAPFree t_1) t.card Nat.findGreatest (fun (m : ) => tu, t.card = m ThreeAPFree t) u.card
      def addRothNumber {α : Type u_2} [DecidableEq α] [AddMonoid α] :

      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
      Instances For
        def mulRothNumber {α : Type u_2} [DecidableEq α] [Monoid α] :

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

        Equations
        Instances For
          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 α) :
          ts, t.card = addRothNumber s ThreeAPFree t
          theorem mulRothNumber_spec {α : Type u_2} [DecidableEq α] [Monoid α] (s : Finset α) :
          ts, t.card = mulRothNumber s ThreeGPFree 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.le_mulRothNumber {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {t : Finset α} (hs : ThreeGPFree s) (h : s t) :
          s.card mulRothNumber t
          theorem ThreeAPFree.addRothNumber_eq {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} (hs : ThreeAPFree s) :
          addRothNumber s = s.card
          theorem ThreeGPFree.mulRothNumber_eq {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} (hs : ThreeGPFree 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
          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_threeAPFree {α : Type u_2} [DecidableEq α] [AddMonoid α] {s : Finset α} {n : } (h : tFinset.powersetCard n s, ¬ThreeAPFree t) :
          addRothNumber s < n
          theorem mulRothNumber_lt_of_forall_not_threeGPFree {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {n : } (h : tFinset.powersetCard n s, ¬ThreeGPFree t) :
          mulRothNumber s < n
          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 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 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.

          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.

          @[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

          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
          Instances For
            theorem rothNumberNat_def (n : ) :
            rothNumberNat n = addRothNumber (Finset.range n)
            theorem rothNumberNat_le (N : ) :
            rothNumberNat N N
            theorem rothNumberNat_spec (n : ) :
            tFinset.range n, t.card = rothNumberNat n ThreeAPFree t
            theorem ThreeAPFree.le_rothNumberNat {k : } {n : } (s : Finset ) (hs : ThreeAPFree s) (hsn : xs, 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