Erdős Problem 865

References:

• erdosproblems.com/865
• [CES75] Choi, S. L. G. and Erdős, P. and Szemerédi, E., Some additive and multiplicative problems in number theory. Acta Arith. (1975), 37--50.

theorem Erdos865.erdos_865 : ∃ C > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ∀ A ⊆ Finset.Icc 1 N, ↑A.card ≥ 5 / 8 * ↑N + C → ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ a + b ∈ A ∧ a + c ∈ A ∧ b + c ∈ A

There exists a constant $C>0$ such that, for all large $N$, if $A\subseteq \{1,\ldots,N\}$ has size at least $\frac{5}{8}N+C$ then there are distinct $a,b,c\in A$ such that $a+b,a+c,b+c\in A$.

A problem of Erdős and Sós (also earlier considered by Choi, Erdős, and Szemerédi [CES75], but Erdős had forgotten this).

theorem Erdos865.erdos_865.variants.k2 (N : ℕ) (A : Finset ℕ) : A ⊆ Finset.Icc 1 (2 * N) → A.card ≥ N + 2 → ∃ a ∈ A, ∃ b ∈ A, a ≠ b ∧ a + b ∈ A

It is a classical folklore fact that if $A\subseteq \{1,\ldots,2N\}$ has size $\geq N+2$ then there are distinct $a,b\in A$ such that $a+b\in A$, which establishes the $k=2$ case.

noncomputable def Erdos865.f (N k : ℕ) : ℕ

Equations

• Erdos865.f N k = sInf {m : ℕ | ∀ A ⊆ Finset.Icc 1 N, A.card ≥ m → ∃ S ⊆ A, S.card = k ∧ ∀ x ∈ S, ∀ y ∈ S, x ≠ y → x + y ∈ A}

theorem Erdos865.erdos_865.variants.sos (k : ℕ) (hk : 2 ≤ k) : Asymptotics.IsEquivalent Filter.atTop (fun (N : ℕ) => ↑(f N k)) fun (N : ℕ) => 1 / 2 * (1 + ∑ r ∈ Finset.Icc 1 (k - 2), (1 / 4) ^ r) * ↑N

Erdős and Sós conjectured that $f_k(N)\sim \frac{1}{2}\left(1+\sum_{1\leq r\leq k-2}\frac{1}{4^r}\right) N$, where $f_k(N)$ is the minimal size of a subset of $\{1, \dots, N\}$ guaranteeing $k$ elements have all pairwise sums in the set.

theorem Erdos865.erdos_865.variants.upper_bound (k : ℕ) (hk : 3 ≤ k) : ∃ ε > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ↑(f N k) ≤ (2 / 3 - ε) * ↑N

Choi, Erdős, and Szemerédi [CES75] have proved that, for all $k\geq 3$, there exists $\epsilon_k>0$ such that (for large enough $N$) $f_k(N)\leq \left(\frac{2}{3}-\epsilon_k\right)N$.