Erdős problem 1192

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$ ?

Sources

The source's own material, retained exactly.

7 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1192.lean

Retained formal statement4 of 7

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

FormalConjectures/ErdosProblems/1192.leanErdos1192.erdos_1192.f_r_singleton_self1 lineExact file

1∀ (n : ℕ), Erdos1192.f_r {n} 1 n = 1

TestStatement only, no proof