Erdős Problem 489

Reference: erdosproblems.com/489

def Erdos489.sievedSet (A : Set ℕ) : Set ℕ

The set of positive integers not divisible by any element of A.

Equations

• Erdos489.sievedSet A = {n : ℕ | 0 < n ∧ ∀ a ∈ A, ¬a ∣ n}

noncomputable def Erdos489.GapSumSq (A : Set ℕ) (x : ℕ) : ℝ

The squared-gap sum ∑_{b_i < x} (b_{i+1} - b_i)², where b_i enumerates the positive integers not divisible by any element of A.

Equations

• One or more equations did not get rendered due to their size.

theorem Erdos489.erdos_489 : sorry ↔ ∀ (A : Set ℕ), ((fun (x : ℕ) => ↑{x ∈ Finset.Icc 1 x | x ∈ A}.card) =o[Filter.atTop] fun (x : ℕ) => √↑x) → (sievedSet A).Infinite → ∃ (L : ℝ), Filter.Tendsto (fun (x : ℕ) => GapSumSq A x / ↑x) Filter.atTop (nhds L)

Let $A\subseteq \mathbb{N}$ be a set such that $\lvert A\cap [1,x]\rvert=o(x^{1/2})$. Let $B=\{ n\geq 1 : a\nmid n\textrm{ for all }a\in A\}$. If $B=\{b_1 < b_2 < \cdots\}$ then is it true that $$\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=\{p^2: p\textrm{ prime}\}$ then $B$ is the set of squarefree numbers, and the existence of this limit was proved by Erdős.

See also [208].

theorem Erdos489.erdos_489.variants.squarefree : ∃ (L : ℝ), Filter.Tendsto (fun (x : ℕ) => GapSumSq {n : ℕ | ∃ (p : ℕ), Nat.Prime p ∧ n = p ^ 2} x / ↑x) Filter.atTop (nhds L)

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.