Erdős Problem 1097

Reference: erdosproblems.com/1097

def Erdos1097.CommonDifferencesThreeTermAP (A : Finset ℤ) : Set ℤ

Given a finite set of integers A (modelled as a Finset ℤ), the set CommonDifferencesThreeTermAP A consists of all integers d such that there is a non-trivial three-term arithmetic progression a, b, c ∈ A with b - a = d and c - b = d.

Equations

• Erdos1097.CommonDifferencesThreeTermAP A = {d : ℤ | d ≠ 0 ∧ ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, b - a = d ∧ c - b = d}

theorem Erdos1097.erdos_1097 : sorry ↔ ∃ C > 0, ∀ (A : Finset ℤ), ↑(CommonDifferencesThreeTermAP A).ncard ≤ C * ↑A.card ^ (3 / 2)

The main conjecture: for any finite set of integers $A$ with $|A| = n$, the number of distinct common differences in three-term arithmetic progressions is $O(n^{3/2})$.

theorem Erdos1097.erdos_1097.variants.weaker (A : Finset ℤ) : (CommonDifferencesThreeTermAP A).ncard ≤ A.card ^ 2

A weaker bound has been proven: there are always at most $n^2$ such values of $d$.

theorem Erdos1097.erdos_1097.variants.lower_bound : ∃ c > 0, ∀ (n : ℕ), ∃ (A : Finset ℤ), A.card = n ∧ c * ↑n ≤ ↑(CommonDifferencesThreeTermAP A).ncard

A trivial lower bound: there exist sets $A$ with $|A| = n$ that contain at least $\Omega(n)$ distinct common differences of three-term arithmetic progressions.