Skip to content

Erdős problem 154

Let A{1,,N}A\subset \{1,\ldots,N\} be a Sidon set with AN1/2\lvert A\rvert\sim N^{1/2}. Must A+AA+A be well-distributed over all small moduli? In particular, must about half the elements of A+AA+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 statement1 of 2

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

The answer is yes. Lindström [Li98] proved the analogous statement for AA itself (see erdos_154.variants.lindstrom), later strengthened by Kolountzakis [Ko99]; well-distribution of A+AA+A then follows using the Sidon property.

We state the question for the sumset: for any sequence of Sidon sets Ak{0,,Nk}A_k\subseteq\{0,\ldots,N_k\} with NkN_k\to\infty and AkNk1/2\lvert A_k\rvert\sim N_k^{1/2}, and any modulus m2m\geq 2, the proportion of elements of Ak+AkA_k+A_k congruent to i(modm)i\pmod m (i.e. the count divided by Ak+Ak\lvert A_k+A_k\rvert) tends to 1/m1/m for every residue i<mi<m.

FormalConjectures/ErdosProblems/154.leanErdos154.erdos_15411 linesExact file
True  ∀ (m : ℕ),    2 ≤ m      ∀ (N : ℕ → ℕ) (A : ℕ → Finset ℕ),        Filter.Tendsto (fun k => ↑(N k)) Filter.atTop Filter.atTop          (∀ (k x : ℕ), xA kxN k) →            (∀ (k : ℕ), IsSidon ↑(A k)) →              Filter.Tendsto (fun k => ↑(A k).card / √↑(N k)) Filter.atTop (nhds 1) →i < m,                  Filter.Tendsto (fun k => ↑{sA k + A k | s % m = i}.card / ↑(A k + A k).card) 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.

Search problems.science

Find a Problem, Result, source, or page