Skip to content

Erdős problem 1192

Does there exist, for all r2r\geq 2, a basis AA of order rr (so that fr(n)>0f_r(n)>0 for all large nn) such that nxfr(n)2x\sum_{n\leq x}f_r(n)^2 \ll x for all xx?

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

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

FormalConjectures/ErdosProblems/1192.leanErdos1192.erdos_1192.f_r_zero_zero1 lineExact file
∀ (A : Set ℕ), Erdos1192.f_r A 0 0 = 1
TestStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page