Skip to content

Erdős problem 1192

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

Sources

The source's own material, retained exactly.

7 retained statements36c6d0fef71a

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 AA such that ∑n≤xfr(n)2≪x\sum_{n\leq x}f_r(n)^2 \ll x and ∣A∩[1,x]∣≫x1/r\lvert A\cap [1,x]\rvert\gg x^{1/r} for all xx.

FormalConjectures/ErdosProblems/1192.leanErdos1192.erdos_1192.variants.renyi4 linesExact file
∀ r ≥ 2,  ∃ A,    ((fun x => ∑ n ∈ Finset.range (x + 1), ↑(Erdos1192.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)
SolvedStatement only, no proof