Erdős Problem 1192

References:

• erdosproblems.com/1192
• [Ru90] Ruzsa, Imre Z., A just basis. Monatsh. Math. (1990), 145--151.
• [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. 6 (1980), 89--115.

noncomputable def Erdos1192.f_r (A : Set ℕ) (r n : ℕ) : ℕ

For $A\subset \mathbb{N}$ let $f_r(n)$ count the number of solutions to $n=a_1+\cdots+a_r$ with $a_i\in A$.

Equations

• Erdos1192.f_r A r n = {v : Fin r → ℕ | (∀ (i : Fin r), v i ∈ A) ∧ ∑ i : Fin r, v i = n}.ncard

theorem Erdos1192.erdos_1192.f_r_zero_zero (A : Set ℕ) : f_r A 0 0 = 1

The empty sum ($r = 0$) gives exactly one representation of $0$: the empty tuple.

theorem Erdos1192.erdos_1192.f_r_empty (r n : ℕ) : f_r ∅ (r + 1) n = 0

With an empty set, there are no valid $r$-tuples for $r \geq 1$.

theorem Erdos1192.erdos_1192.f_r_singleton_self (n : ℕ) : f_r {n} 1 n = 1

For $r = 1$, $f_1(\{n\}, n) = 1$: the only $1$-tuple from $\{n\}$ summing to $n$ is $(n)$.

theorem Erdos1192.erdos_1192.f_r_no_rep : f_r {0} 1 1 = 0

$f_1(\{0\}, 1) = 0$: can't represent $1$ with a single element from $\{0\}$.

theorem Erdos1192.erdos_1192 : sorry ↔ ∀ r ≥ 2, ∃ (A : Set ℕ), (∀ᶠ (n : ℕ) in Filter.atTop, f_r A r n > 0) ∧ (fun (x : ℕ) => ∑ n ∈ Finset.range (x + 1), ↑(f_r A r n) ^ 2) =O[Filter.atTop] fun (x : ℕ) => ↑x

Does there exist, for all $r\geq 2$, a basis $A$ of order $r$ (so that $f_r(n)>0$ for all large $n$) such that $$\sum_{n\leq x}f_r(n)^2 \ll x$$ for all $x$?

theorem Erdos1192.erdos_1192.variants.renyi (r : ℕ) : r ≥ 2 → ∃ (A : Set ℕ), ((fun (x : ℕ) => ∑ n ∈ Finset.range (x + 1), ↑(f_r A r n) ^ 2) =O[Filter.atTop] fun (x : ℕ) => ↑x) ∧ (fun (x : ℕ) => ↑x ^ (1 / ↑r)) =O[Filter.atTop] fun (x : ℕ) => ↑(Nat.count A x)

Erdős and Rényi proved by the probabilistic method that there exists a set $A$ such that $$\sum_{n\leq x}f_r(n)^2 \ll x$$ and $$\lvert A\cap [1,x]\rvert\gg x^{1/r}$$ for all $x$.

theorem Erdos1192.erdos_1192.variants.ruzsa : ∃ (A : Set ℕ), (∀ᶠ (n : ℕ) in Filter.atTop, f_r A 2 n > 0) ∧ (fun (x : ℕ) => ∑ n ∈ Finset.range (x + 1), ↑(f_r A 2 n) ^ 2) =O[Filter.atTop] fun (x : ℕ) => ↑x

Ruzsa [Ru90] proved that the answer is yes for $r=2$.