Erdős Problem 14

Reference: erdosproblems.com/14

@[reducible, inline]

abbrev Erdos14.allUniqueSums (A : Set ℕ) : Set ℕ

Equations

• Erdos14.allUniqueSums A = {n : ℕ | ∃! a : ℕ × ℕ, a.1 ≤ a.2 ∧ a.1 ∈ A ∧ a.2 ∈ A ∧ a.1 + a.2 = n}

noncomputable def Erdos14.nonUniqueSumCount (A : Set ℕ) (N : ℕ) : ℝ

The number of integers in $\{1,\ldots,N\}$ which are not representable in exactly one way as the sum of two elements from $A$ (either because they are not representable at all, or because they are representable in more than one way).

Equations

• Erdos14.nonUniqueSumCount A N = ↑(Set.Icc 1 N \ Erdos14.allUniqueSums A).ncard

noncomputable def Erdos14.almostSquareRoot (ε : ℝ) (N : ℕ) : ℝ

Equations

• Erdos14.almostSquareRoot ε N = ↑N ^ (1 / 2 - ε)

noncomputable def Erdos14.squareRoot (N : ℕ) : ℝ

Equations

• Erdos14.squareRoot N = √↑N

theorem Erdos14.erdos_14a : (∀ (A : Set ℕ), ∀ ε > 0, almostSquareRoot ε ≪ nonUniqueSumCount A) ↔ sorry

Let $A ⊆ \mathbb{N}$. Let $B ⊆ \mathbb{N}$ be the set of integers which are representable in exactly one way as the sum of two elements from $A$. Is it true that for all $\epsilon > 0$ and large $N$, $|\{1,\ldots,N\} \setminus B| \gg_\epsilon N^{1/2 - \epsilon}$?

theorem Erdos14.erdos_14b : ∃ (A : Set ℕ), nonUniqueSumCount A =o[Filter.atTop] squareRoot ↔ sorry

Is it possible that $|\{1,\ldots,N\} \setminus B| = o(N^\frac{1}{2})$?