Erdős problem 1192 · problems.science

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

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

7 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1192.lean

Retained formal statement6 of 7

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

FormalConjectures/ErdosProblems/1192.leanErdos1192.erdos_1192.variants.renyi4 linesExact file

1∀ r ≥ 2,2  ∃ A,3    ((fun x => ∑ n ∈ Finset.range (x + 1), ↑(Erdos1192.f_r A r n) ^ 2) =O[Filter.atTop] fun x => ↑x) ∧4      (fun x => ↑x ^ (1 / ↑r)) =O[Filter.atTop] fun x => ↑(Nat.count A x)

SolvedStatement only, no proof

Sources

Search problems.science