Erdős problem 489

If $A$ is a forbidden-divisor set with $|A \cap [1,x]| = o(\sqrt{x})$ and $B = \{b_1 < b_2 < \cdots\}$ the sifted set, must $x^{-1} \sum_{b_i < x} (b_{i+1} - b_i)^2$ converge to a finite limit?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

489.lean

Retained formal statement2 of 2

When $A = \{p^2 : p \textrm{ prime}\}$ , $B$ is the set of squarefree numbers, and the existence of this limit was proved by Erdős. This is the $\alpha = 2$ case of Erdős Problem 145.

FormalConjectures/ErdosProblems/489.leanErdos489.erdos_489.variants.squarefree1 lineExact file

1∃ L, Filter.Tendsto (fun x => Erdos489.GapSumSq {n | ∃ p, Nat.Prime p ∧ n = p ^ 2} x / ↑x) Filter.atTop (nhds L)

SolvedStatement only, no proof