Erdős problem 154 · problems.science

Let $A\subset \{1,\ldots,N\}$ be a Sidon set with $\lvert A\rvert\sim N^{1/2}$ . Must $A+A$ be well-distributed over all small moduli? In particular, must about half the elements of $A+A$ be even and half odd?

Sources

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

154.lean

Retained formal statement2 of 2

Lindström's result for $A$ itself [Li98], later strengthened by Kolountzakis [Ko99]: for any sequence of Sidon sets $A_k\subseteq\{0,\ldots,N_k\}$ with $N_k\to\infty$ and $\lvert A_k\rvert\sim N_k^{1/2}$ , and any modulus $m\geq 2$ , the number of elements of $A_k$ congruent to $i\pmod m$ , divided by $N_k^{1/2}$ , tends to $1/m$ for every residue $i<m$ .

Well-distribution of $A+A$ (the actual question, erdos_154) follows from this using the Sidon property.

FormalConjectures/ErdosProblems/154.leanErdos154.erdos_154.variants.lindstrom8 linesExact file

1∀ (m : ℕ),2  2 ≤ m →3    ∀ (N : ℕ → ℕ) (A : ℕ → Finset ℕ),4      Filter.Tendsto (fun k => ↑(N k)) Filter.atTop Filter.atTop →5        (∀ (k x : ℕ), x ∈ A k → x ≤ N k) →6          (∀ (k : ℕ), IsSidon ↑(A k)) →7            Filter.Tendsto (fun k => ↑(A k).card / √↑(N k)) Filter.atTop (nhds 1) →8              ∀ i < m, Filter.Tendsto (fun k => ↑{a ∈ A k | a % m = i}.card / √↑(N k)) Filter.atTop (nhds (1 / ↑m))

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science