Documentation

Mathlib.Combinatorics.Additive.SalemSpencer

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 #

TODO #

Tags #

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

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

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
Instances For
    def MulSalemSpencer {α : Type u_2} [Monoid α] (s : 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.

    Equations
    Instances For
      theorem instDecidableAddSalemSpencerToSet.proof_1 {α : Type u_1} [AddMonoid α] {s : Finset α} :
      (as, bs, cs, a + b = c + ca = b) AddSalemSpencer s

      Whether a given finset is Salem-Spencer is decidable.

      Equations
      • instDecidableAddSalemSpencerToSet = decidable_of_iff (as, bs, cs, a + b = c + ca = b)

      Whether a given finset is Salem-Spencer is decidable.

      Equations
      • instDecidableMulSalemSpencerToSet = decidable_of_iff (as, bs, cs, a * b = c * ca = b)
      theorem AddSalemSpencer.mono {α : Type u_2} [AddMonoid α] {s : Set α} {t : Set α} (h : t s) (hs : AddSalemSpencer s) :
      theorem MulSalemSpencer.mono {α : Type u_2} [Monoid α] {s : Set α} {t : Set α} (h : t s) (hs : MulSalemSpencer s) :
      @[simp]
      @[simp]
      theorem addSalemSpencer_singleton {α : Type u_2} [AddMonoid α] (a : α) :
      @[simp]
      theorem mulSalemSpencer_singleton {α : Type u_2} [Monoid α] (a : α) :
      theorem AddSalemSpencer.prod {α : Type u_2} {β : Type u_3} [AddMonoid α] [AddMonoid β] {s : Set α} {t : Set β} (hs : AddSalemSpencer s) (ht : AddSalemSpencer t) :
      theorem MulSalemSpencer.prod {α : Type u_2} {β : Type u_3} [Monoid α] [Monoid β] {s : Set α} {t : Set β} (hs : MulSalemSpencer s) (ht : MulSalemSpencer 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)) :
      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)) :
      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) :
      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) :
      theorem addSalemSpencer_insert {α : Type u_2} [AddCancelCommMonoid α] {s : Set α} {a : α} :
      AddSalemSpencer (insert a s) AddSalemSpencer s (∀ ⦃b c : α⦄, b sc sa + b = c + ca = b) ∀ ⦃b c : α⦄, b sc sb + c = a + ab = c
      theorem mulSalemSpencer_insert {α : Type u_2} [CancelCommMonoid α] {s : Set α} {a : α} :
      MulSalemSpencer (insert a s) MulSalemSpencer s (∀ ⦃b c : α⦄, b sc sa * b = c * ca = b) ∀ ⦃b c : α⦄, b sc sb * c = a * ab = c
      @[simp]
      theorem addSalemSpencer_pair {α : Type u_2} [AddCancelCommMonoid α] (a : α) (b : α) :
      @[simp]
      theorem mulSalemSpencer_pair {α : Type u_2} [CancelCommMonoid α] (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 : is, i < a) :
      AddSalemSpencer (insert a s) AddSalemSpencer s ∀ ⦃b c : α⦄, b sc sa + b = c + ca = b
      theorem mulSalemSpencer_insert_of_lt {α : Type u_2} [OrderedCancelCommMonoid α] {s : Set α} {a : α} (hs : is, i < a) :
      MulSalemSpencer (insert a s) MulSalemSpencer s ∀ ⦃b c : α⦄, b sc sa * b = c * ca = 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 sb sc sa + b = c + ca = 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) :

      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.

      def addRothNumber {α : Type u_2} [DecidableEq α] [AddMonoid α] :

      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
      Instances For
        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 α] :

        The multiplicative Roth number of a finset is the cardinality of its biggest multiplicative Salem-Spencer 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 α) :
          ∃ (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 )motive x
          Equations
          • =
          Instances For
            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 : tFinset.powersetCard n s, ¬AddSalemSpencer t) :
            addRothNumber s < n
            theorem mulRothNumber_lt_of_forall_not_mulSalemSpencer {α : Type u_2} [DecidableEq α] [Monoid α] {s : Finset α} {n : } (h : tFinset.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

            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 : ) :
              ∃ (t : Finset ) (_ : t Finset.range n), t.card = rothNumberNat n AddSalemSpencer t
              theorem AddSalemSpencer.le_rothNumberNat {k : } {n : } (s : Finset ) (hs : AddSalemSpencer s) (hsn : xs, 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).