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 statement7 of 7

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

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

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

SolvedStatement only, no proof

Sources

Search problems.science