Number of arithmetic progressions in dense sets

DefinitionContaining a \(k\)-term arithmetic progression#✓fully proved

A finite set \(A \subseteq \mathbb{N}\) contains a \(k\)-term arithmetic progression when there are natural numbers \(a\) and \(d \ge 1\) with \(a + i d \in A\) for every natural number \(i < k\), that is, \(a, a + d, \dots, a + (k - 1) d\) all lie in \(A\). For \(k = 0\) this holds vacuously.

def HasAP (A : Finset ℕ) (k : ℕ) : Prop :=
  ∃ a d : ℕ, 0 < d ∧ ∀ i < k, a + i * d ∈ A

Used by 1

Used byThe progression threshold \(F_k(N, \ell)\)

DefinitionNumber of \(k\)-term arithmetic progressions in a set#✓fully proved

For a finite set \(A \subseteq \mathbb{N}\) and a natural number \(k\), \(\mathrm{AP}_k(A)\) is the number of pairs \((a, d)\) of natural numbers with \(a \in A\) and \(1 \le d \le \max A\) such that \(a + i d \in A\) for every natural number \(i < k\). For \(k \ge 2\) the conditions \(a \in A\) and \(d \le \max A\) follow from the others, so \(\mathrm{AP}_k(A)\) counts the \(k\)-term progressions \(a, a + d, \dots, a + (k - 1) d\) in \(A\) with \(d \ge 1\).

def apCount (A : Finset ℕ) (k : ℕ) : ℕ :=
  ((A ×ˢ Finset.Icc 1 (A.sup id)).filter (fun p => ∀ i < k, p.1 + i * p.2 ∈ A)).card

Used by 1

Used byThe progression threshold \(F_k(N, \ell)\)

DefinitionThe progression threshold \(F_k(N, \ell)\)#✓fully proved

For natural numbers \(k\), \(\ell\) and \(N\), \(F_k(N, \ell)\) is the least natural number \(m\) such that every \(N\)-element set \(A \subseteq \mathbb{N}\) with \(\mathrm{AP}_k(A) \ge m\) contains an \(\ell\)-term arithmetic progression, where \(\mathrm{AP}_k(A)\) is the number of pairs \((a, d)\) with \(a \in A\), \(1 \le d \le \max A\) and \(a + i d \in A\) for all \(i < k\) (for \(k \ge 2\), the number of \(k\)-term progressions in \(A\) with \(d \ge 1\)); if no such \(m\) exists, \(F_k(N, \ell) = 0\).

For \(k \ge 2\) such an \(m\) always exists, since an \(N\)-element set has at most \(N^2\) \(k\)-term progressions.

noncomputable def apThreshold (k ℓ N : ℕ) : ℕ :=
  sInf {m : ℕ | ∀ A : Finset ℕ, A.card = N → m ≤ apCount A k → HasAP A ℓ}

Uses 2 · Used by 2

Statement usesContaining a \(k\)-term arithmetic progression · Number of \(k\)-term arithmetic progressions in a set

Used byErdős Problem 179: does \(\log F_3(N, \ell) / \log N\) tend to \(2\)? · Erdős Problem 179: is \(F_3(N, 4) = o(N^2)\)?

DefinitionErdős Problem 179: is \(F_3(N, 4) = o(N^2)\)?#✓fully proved

Erdős Problem 179: is \(F_3(N, 4) = o(N^2)\)? The statement that \(F_3(N, 4) = o(N^2)\) as \(N \to \infty\) over the natural numbers, that is, \(F_3(N, 4) / N^2 \to 0\), where \(F_3(N, 4)\) is the least \(m\) such that every \(N\)-element set \(A \subseteq \mathbb{N}\) containing at least \(m\) three-term arithmetic progressions \(a, a + d, a + 2d\) with \(d \ge 1\) contains a \(4\)-term arithmetic progression.

def threeAPThresholdForFourAPLittleO : Prop :=
  (fun N : ℕ => (apThreshold 3 4 N : ℝ)) =o[atTop] (fun N : ℕ => (N : ℝ) ^ 2)

Uses 1 · Used by 1

Statement usesThe progression threshold \(F_k(N, \ell)\)

Used byErdős Problem 179: \(F_3(N, 4) = o(N^2)\)

DefinitionErdős Problem 179: does \(\log F_3(N, \ell) / \log N\) tend to \(2\)?#✓fully proved

Erdős Problem 179: does \(\log F_3(N, \ell) / \log N\) tend to \(2\)? The statement that for every natural number \(\ell > 3\), \(\log F_3(N, \ell) / \log N \to 2\) as \(N \to \infty\) over the natural numbers, where \(F_3(N, \ell)\) is the least \(m\) such that every \(N\)-element set \(A \subseteq \mathbb{N}\) containing at least \(m\) three-term arithmetic progressions \(a, a + d, a + 2d\) with \(d \ge 1\) contains an \(\ell\)-term arithmetic progression.

def threeAPThresholdExponentTwo : Prop :=
  ∀ ℓ : ℕ, 3 < ℓ →
    Tendsto (fun N : ℕ => Real.log (apThreshold 3 ℓ N) / Real.log N) atTop (𝓝 2)

Uses 1 · Used by 1

Statement usesThe progression threshold \(F_k(N, \ell)\)

Used byErdős Problem 179: \(\log F_3(N, \ell) / \log N\) tends to \(2\)

TheoremErdős Problem 179: \(F_3(N, 4) = o(N^2)\)#●ready to prove

As \(N \to \infty\) over the natural numbers, \(F_3(N, 4) / N^2 \to 0\), that is, \(F_3(N, 4) = o(N^2)\), where \(F_3(N, 4)\) is the least natural number \(m\) such that every \(N\)-element set \(A \subseteq \mathbb{N}\) containing at least \(m\) three-term arithmetic progressions \(a, a + d, a + 2d\) with \(d \ge 1\) contains a \(4\)-term arithmetic progression.

Write \(F_k(N, \ell)\) for the same threshold with \(k\)-term progressions in place of three-term ones and \(\ell\)-term progressions in place of \(4\)-term ones. Fox and Pohoata bound \(F_k(N, \ell)\) above by \((r_\ell(N) / N)^{O(1)} N^2\), where \(r_\ell(N)\) is the largest size of a subset of \(\{1, \dots, N\}\) without \(\ell\)-term progressions; since \(r_\ell(N) = o(N)\) by Szemerédi's theorem, this bound is \(o(N^2)\). erdosproblems.com/179 records \(F_k(N, \ell) \le N^2 / (\log \log N)^{C_\ell}\) for a constant \(C_\ell\) depending only on \(\ell\).

public theorem_wanted threeAPThresholdForFourAPLittleO_holds : threeAPThresholdForFourAPLittleO

Sources

• T. F. Bloom, Erdős Problems, Problem #179, https://www.erdosproblems.com/179 (status PROVED); resolution: J. Fox and C. Pohoata, Sets without k-term progressions can have many shorter progressions, Random Structures Algorithms 58 (2021), 383-389, arXiv:1908.09905, main theorem: for all k > s ≥ 3, log f_{s,k}(n) / log n → 2, where f_{s,k}(n) = F_s(n, k) - 1 is the largest number of s-term progressions in an n-set with no k-term progression; erdosproblems.com/179: F_k(N, ℓ) ≤ N² / (log log N)^{C_ℓ}, https://arxiv.org/abs/1908.09905.

Uses 1

Statement usesErdős Problem 179: is \(F_3(N, 4) = o(N^2)\)?

TheoremErdős Problem 179: \(\log F_3(N, \ell) / \log N\) tends to \(2\)#●ready to prove

For every natural number \(\ell > 3\), \(\log F_3(N, \ell) / \log N \to 2\) as \(N \to \infty\) over the natural numbers, where \(F_3(N, \ell)\) is the least natural number \(m\) such that every \(N\)-element set \(A \subseteq \mathbb{N}\) containing at least \(m\) three-term arithmetic progressions \(a, a + d, a + 2d\) with \(d \ge 1\) contains an \(\ell\)-term arithmetic progression.

Fox and Pohoata prove that \(\log f_{s,k}(n) / \log n \to 2\) for all \(k > s \ge 3\), where \(f_{s,k}(n)\) is the largest number of \(s\)-term progressions in an \(n\)-element set with no \(k\)-term progression; since \(F_3(N, \ell) = f_{3,\ell}(N) + 1\), taking \(s = 3\) and \(k = \ell\) gives the statement.

public theorem_wanted threeAPThresholdExponentTwo_holds : threeAPThresholdExponentTwo

Sources

• T. F. Bloom, Erdős Problems, Problem #179, https://www.erdosproblems.com/179 (status PROVED); resolution: J. Fox and C. Pohoata, Sets without k-term progressions can have many shorter progressions, Random Structures Algorithms 58 (2021), 383-389, arXiv:1908.09905, main theorem: for all k > s ≥ 3, log f_{s,k}(n) / log n → 2, where f_{s,k}(n) = F_s(n, k) - 1 is the largest number of s-term progressions in an n-set with no k-term progression; erdosproblems.com/179: F_k(N, ℓ) ≤ N² / (log log N)^{C_ℓ}, https://arxiv.org/abs/1908.09905.

Uses 1

Statement usesErdős Problem 179: does \(\log F_3(N, \ell) / \log N\) tend to \(2\)?

5 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.