Arithmetic progressions and progression-free sets

DefinitionSet arithmetic progressions with given first term and difference#✓fully proved

Let \(M\) be an additive commutative monoid, \(l \in \mathbb{N} \cup \{\infty\}\) and \(a, d \in M\). A set \(s \subseteq M\) is an arithmetic progression of length \(l\) with first term \(a\) and difference \(d\) if \(s = \{a + n d : n \in \mathbb{N},\ n < l\}\) and \(s\) has exactly \(l\) elements, counting the size of an infinite set as \(\infty\); here \(n d\) is the sum of \(n\) copies of \(d\).

def Set.IsAPOfLengthWith (s : Set α) (l : ℕ∞) (a d : α) : Prop :=
  ENat.card s = l ∧ s = {a + n • d | (n : ℕ) (_ : n < l)}

Used by 10

Used byCardinality of a set arithmetic progression · First term and difference of a set arithmetic progression · Sets that are arithmetic progressions · Sets of naturals without three-term progressions · Nathanson's bound for restricted sumsets and its inverse · Inverse theorem for the extremal restricted signed sumset of positive integers · Inverse theorem for the extremal restricted signed sumset of sets containing zero · Arithmetic progressions with a common difference · Vosper's theorem · Counting arithmetic progressions in \(\{1, \dots, n\}\)

DefinitionSets that are arithmetic progressions#✓fully proved

Let \(\alpha\) be an additive commutative monoid and \(l \in \mathbb{N} \cup \{\infty\}\). A set \(s \subseteq \alpha\) is an arithmetic progression of length \(l\) if there are \(a, d \in \alpha\) such that \(s = \{a + nd : n \in \mathbb{N},\ n < l\}\) and \(s\) has exactly \(l\) elements (infinitely many when \(l = \infty\)). Here \(nd\) denotes the sum of \(n\) copies of \(d\).

def Set.IsAPOfLength (s : Set α) (l : ℕ∞) : Prop :=
  ∃ a d : α, s.IsAPOfLengthWith l a d

Uses 1 · Used by 15

Statement usesSet arithmetic progressions with given first term and difference

Used byCardinality of a set arithmetic progression · First term and difference of a set arithmetic progression · Progression-free sets · Sets of naturals without three-term progressions · A largest progression-free subset is attained · A progression of length greater than one is not progression-free · Lower bound and inverse theorem for sums with at least \(r\) distinct terms in \(\mathbb{Z}\) · Inverse theorem for sums with at least \(r\) distinct terms modulo a prime · Freiman's \(3k - 4\) theorem · Nathanson's inverse theorem for restricted sumsets · Vosper's theorem for iterated sumsets · Yang–Chen inverse theorem for at least five terms · Yang–Chen inverse theorem for three terms · Yang–Chen inverse theorem for four terms · Erdős Problem 966: progression-free sets that are Ramsey for shorter progressions

TheoremCardinality of a set arithmetic progression#✓fully proved

Let \(M\) be an additive commutative monoid and \(l \in \mathbb{N} \cup \{\infty\}\). If a set \(s \subseteq M\) is an arithmetic progression of length \(l\), then \(s\) has exactly \(l\) elements, counting the size of an infinite set as \(\infty\).

theorem card (h : s.IsAPOfLength l) : ENat.card s = l

Uses 2 · Used by 1

Statement usesSets that are arithmetic progressions

Proof usesSet arithmetic progressions with given first term and difference

Used byA largest progression-free subset is attained

TheoremFirst term and difference of a set arithmetic progression#✓fully proved

Let \(M\) be an additive commutative monoid and \(l \in \mathbb{N} \cup \{\infty\}\). If a set \(s \subseteq M\) is an arithmetic progression of length \(l\), then there are \(a, d \in M\) with \(s = \{a + n d : n \in \mathbb{N},\ n < l\}\), where \(n d\) is the sum of \(n\) copies of \(d\).

theorem eq (h : s.IsAPOfLength l) :
    ∃ a d : α, s = {a + n • d | (n : ℕ) (_ : n < l)}

Uses 2

Statement usesSets that are arithmetic progressions

Proof usesSet arithmetic progressions with given first term and difference

DefinitionList arithmetic progressions with given start and difference#✓fully proved

Let \(M\) be an additive commutative monoid, \(l \in \mathbb{N}\) and \(a, d \in M\). A list \(s\) of elements of \(M\) is an arithmetic progression of length \(l\) starting from \(a\) with difference \(d\), in either direction, if \(s = (a, a + d, \dots, a + (l - 1)d)\) or \(s = (a + (l - 1)d, \dots, a + d, a)\), where \(n d\) is the sum of \(n\) copies of \(d\); when \(l = 0\) both lists are empty.

def List.IsAPOfLengthWith (s : List α) (l : ℕ) (a d : α) : Prop :=
  s = (List.range l).map (fun n ↦ a + n • d) ∨
    s = (List.range l).reverse.map (fun n ↦ a + n • d)

Used by 1

Used byArithmetic progressions of lists

DefinitionArithmetic progressions of lists#✓fully proved

Let \(M\) be an additive commutative monoid and \(l \in \mathbb{N}\). A list \(s\) of elements of \(M\) is an arithmetic progression of length \(l\) if there are \(a, d \in M\) such that \(s = (a, a + d, \dots, a + (l - 1)d)\) or \(s = (a + (l - 1)d, \dots, a + d, a)\), where \(n d\) is the sum of \(n\) copies of \(d\).

def List.IsAPOfLength (s : List α) (l : ℕ) : Prop :=
  ∃ a d : α, s.IsAPOfLengthWith l a d

Uses 1 · Used by 1

Statement usesList arithmetic progressions with given start and difference

Used byMonotone arithmetic progressions in a function

DefinitionMonotone arithmetic progressions in a function#✓fully proved

Let \(M\) be an additive commutative monoid, \(\beta\) a preordered type, \(f : \beta \to M\) and \(k \in \mathbb{N}\). Then \(f\) contains a monotone arithmetic progression of length \(k\) if there are \(x_1 < x_2 < \dots < x_k\) in \(\beta\) such that the list \((f(x_1), \dots, f(x_k))\) is an arithmetic progression of length \(k\): for some \(a, d \in M\) it equals \((a, a + d, \dots, a + (k - 1)d)\) or its reverse.

def HasMonotoneAP {β : Type*} [Preorder β] (f : β → α) (k : ℕ) : Prop :=
  ∃ l : List β, (l.map f).IsAPOfLength k ∧ l.Pairwise (· < ·)

Uses 1

Statement usesArithmetic progressions of lists

DefinitionProgression-free sets#✓fully proved

Let \(M\) be an additive commutative monoid and \(l \in \mathbb{N} \cup \{\infty\}\). A set \(s \subseteq M\) is free of nontrivial arithmetic progressions of length \(l\) if every subset of \(s\) that is an arithmetic progression of length \(l\) forces \(l \le 1\); equivalently, \(l \le 1\) or no subset of \(s\) is an arithmetic progression of length \(l\).

def Set.IsAPOfLengthFree (s : Set α) (l : ℕ∞) : Prop :=
  ∀ t ⊆ s, t.IsAPOfLength l → l ≤ 1

Uses 1 · Used by 4

Statement usesSets that are arithmetic progressions

Used byProgression-free finite sets · Sets of naturals without three-term progressions · A progression of length greater than one is not progression-free · Erdős Problem 966: progression-free sets that are Ramsey for shorter progressions

TheoremA progression of length greater than one is not progression-free#✓fully proved

Let \(s\) be a set in an additive commutative monoid and \(l \in \mathbb{N} \cup \{\infty\}\) with \(l > 1\). If \(s\) is an arithmetic progression of length \(l\), then \(s\) is not free of nontrivial arithmetic progressions of length \(l\).

theorem Set.IsAPOfLength.not_isAPOfLengthFree {s : Set α} {l : ℕ∞}
    (hs : s.IsAPOfLength l) (hl : 1 < l) : ¬ s.IsAPOfLengthFree l

Uses 2

Statement usesSets that are arithmetic progressions · Progression-free sets

DefinitionProgression-free finite sets#✓fully proved

Let \(M\) be an additive commutative monoid and \(l \in \mathbb{N} \cup \{\infty\}\). A finite set \(s \subseteq M\) is free of nontrivial arithmetic progressions of length \(l\) if it is so as a set: \(l \le 1\), or no subset of \(s\) is an arithmetic progression of length \(l\).

def Finset.IsAPOfLengthFree (s : Finset α) (l : ℕ∞) : Prop :=
  (s : Set α).IsAPOfLengthFree l

Uses 1 · Used by 4

Statement usesProgression-free sets

Used byProgression-free subsets are bounded by the extremal size · Largest size of a progression-free subset of \(\{1, \dots, N\}\) · Trivial upper bound for the largest progression-free subset · A largest progression-free subset is attained

TheoremSets of naturals without three-term progressions#✓fully proved

Let \(s\) be a set of natural numbers such that \(a = b\) whenever \(a, b, c \in s\) satisfy \(a + c = 2b\). Then \(s\) is free of nontrivial arithmetic progressions of length \(3\): no subset of \(s\) is an arithmetic progression of length \(3\).

theorem ThreeAPFree.isAPOfLengthFree_three {s : Set ℕ} (hs : ThreeAPFree s) :
    s.IsAPOfLengthFree 3

Uses 3

Statement usesProgression-free sets

Proof usesSets that are arithmetic progressions · Set arithmetic progressions with given first term and difference

DefinitionLargest size of a progression-free subset of \(\{1, \dots, N\}\)#✓fully proved

For natural numbers \(k\) and \(N\), \(r_k(N)\) is the largest cardinality of a subset \(S \subseteq \{1, \dots, N\}\) that is free of nontrivial arithmetic progressions of length \(k\), meaning that if \(k \ge 2\) then no subset of \(S\) is an arithmetic progression of length \(k\) (for \(k \le 1\) every subset qualifies).

noncomputable def Set.IsAPOfLengthFree.maxCard (k N : ℕ) : ℕ :=
  by
    classical
    exact Nat.findGreatest
      (fun m ↦ ∃ S : Finset ℕ,
        S ⊆ Finset.Icc 1 N ∧ S.card = m ∧ S.IsAPOfLengthFree k)
      N

Uses 1 · Used by 3

Statement usesProgression-free finite sets

Used byProgression-free subsets are bounded by the extremal size · Trivial upper bound for the largest progression-free subset · A largest progression-free subset is attained

TheoremTrivial upper bound for the largest progression-free subset#✓fully proved

For all natural numbers \(k\) and \(N\), the largest size \(r_k(N)\) of a subset of \(\{1, \dots, N\}\) free of nontrivial arithmetic progressions of length \(k\) satisfies \(r_k(N) \le N\).

theorem maxCard_le (k N : ℕ) : maxCard k N ≤ N

Uses 2

Statement usesLargest size of a progression-free subset of \(\{1, \dots, N\}\)

Proof usesProgression-free finite sets

TheoremA largest progression-free subset is attained#✓fully proved

For all natural numbers \(k\) and \(N\), let \(r_k(N)\) be the largest size of a subset of \(\{1, \dots, N\}\) free of nontrivial arithmetic progressions of length \(k\). Then some subset \(S \subseteq \{1, \dots, N\}\) free of nontrivial arithmetic progressions of length \(k\) has exactly \(r_k(N)\) elements.

theorem maxCard_spec (k N : ℕ) :
    ∃ S : Finset ℕ, S ⊆ Finset.Icc 1 N ∧
      S.card = maxCard k N ∧ S.IsAPOfLengthFree k

Uses 4

Statement usesProgression-free finite sets · Largest size of a progression-free subset of \(\{1, \dots, N\}\)

Proof usesSets that are arithmetic progressions · Cardinality of a set arithmetic progression

TheoremProgression-free subsets are bounded by the extremal size#✓fully proved

Let \(k\) and \(N\) be natural numbers, and let \(S\) be a finite set of natural numbers with \(S \subseteq \{1, \dots, N\}\) that is free of nontrivial arithmetic progressions of length \(k\). Then \(|S| \le r_k(N)\), where \(r_k(N)\) is the largest size of a subset of \(\{1, \dots, N\}\) containing no nontrivial \(k\)-term arithmetic progression.

theorem card_le_maxCard {S : Finset ℕ} {k N : ℕ}
    (hS : S ⊆ Finset.Icc 1 N) (hfree : S.IsAPOfLengthFree k) :
    S.card ≤ maxCard k N

Uses 2

Statement usesProgression-free finite sets · Largest size of a progression-free subset of \(\{1, \dots, N\}\)

15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.