Skip to content

Erdős problem 489

If AA is a forbidden-divisor set with ∣A∩[1,x]∣=o(x)|A \cap [1,x]| = o(\sqrt{x}) and B={b1<b2<⋯ }B = \{b_1 < b_2 < \cdots\} the sifted set, must x−1∑bi<x(bi+1−bi)2x^{-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

Open selected source

FormalConjectures/ErdosProblems/

489.lean

Retained formal statement1 of 2

Let A⊆NA\subseteq \mathbb{N} be a set such that ∣A∩[1,x]∣=o(x1/2)\lvert A\cap [1,x]\rvert=o(x^{1/2}). Let B={n≥1:a∤n for all a∈A}B=\{ n\geq 1 : a\nmid n\textrm{ for all }a\in A\}. If B={b1<b2<⋯ }B=\{b_1 < b_2 < \cdots\} then is it true that lim⁡x→∞1x∑bi<x(bi+1−bi)2\lim_{x \to \infty} \frac{1}{x}\sum_{b_i < x}(b_{i+1}-b_i)^2 exists (and is finite)?

For example, when A={p2:p prime}A=\{p^2: p\textrm{ prime}\} then BB is the set of squarefree numbers, and the existence of this limit was proved by Erdős.

See also [208].

FormalConjectures/ErdosProblems/489.leanErdos489.erdos_4894 linesExact file
True ↔  ∀ (A : Set ℕ),    ((fun x => ↑{x ∈ Finset.Icc 1 x | x ∈ A}.card) =o[Filter.atTop] fun x => √↑x) →      (Erdos489.sievedSet A).Infinite → ∃ L, Filter.Tendsto (fun x => Erdos489.GapSumSq A x / ↑x) Filter.atTop (nhds L)
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.