Erdős Problem 332

Reference: erdosproblems.com/332

noncomputable def Erdos332.D_A (A : Set ℕ) : Set ℤ

The set of numbers $D(A)$ which occur infinitely often as $a_1 - a_2$ with $a_1, a_2 \in A$.

Equations

• Erdos332.D_A A = {d : ℤ | {(a, b) : ℕ × ℕ | a ∈ A ∧ b ∈ A ∧ ↑a - ↑b = d}.Infinite}

def Erdos332.HasBoundedGaps (S : Set ℤ) : Prop

A set $S \subseteq \mathbb{Z}$ has bounded gaps if it is syndetic, meaning there is a uniform bound $M$ such that every interval of length $M$ contains an element of $S$.

Equations

• Erdos332.HasBoundedGaps S = ∃ M > 0, ∀ (z : ℤ), ∃ s ∈ S, z ≤ s ∧ s < z + ↑M

theorem Erdos332.erdos_332 (A : Set ℕ) : sorry A → HasBoundedGaps (D_A A)

Let $A\subseteq \mathbb{N}$ and $D(A)$ be the set of those numbers which occur infinitely often as $a_1 - a_2$ with $a_1, a_2\in A$. What conditions on $A$ are sufficient to ensure $D(A)$ has bounded gaps?

This is formalised here using the answer(sorry) mechanism. In order to solve this problem one has to provide what the sufficient conditions are, and proof that they imply the desired condition. If the condition is a solution to the problem is up to human judgement.