Erdős Problem 145

Reference: erdosproblems.com/145

@[reducible, inline]

noncomputable abbrev Erdos145.s (n : ℕ) : ℕ

Let $s_1 < s_2 < \cdots$ be the sequence of squarefree numbers.

Equations

• Erdos145.s n = Nat.nth Squarefree n

@[reducible, inline]

noncomputable abbrev Erdos145.A (x : ℝ) : Finset ℕ

Let $A(x)$ denote the set of indices $n$ for which $s_n \leq x$.

Equations

• Erdos145.A x = (Finset.Icc 0 ⌊x⌋₊).preimage Erdos145.s ⋯

theorem Erdos145.erdos_145 : (∀ α ≥ 0, ∃ (β : ℝ), Filter.Tendsto (fun (x : ℝ) => 1 / x * ∑ n ∈ A x, (↑(s (n + 1)) - ↑(s n)) ^ α) Filter.atTop (nhds β)) ↔ sorry

Let $s_1 < s_2 < \cdots$ be the sequence of squarefree numbers. Is it true that, for any $\alpha\geq 0$, $$ \lim_{x\to\infty} \frac{1}{x}\sum_{s_n\leq x}(s_{n+1}-s_n)^\alpha $$ exists?

theorem Erdos145.erdos_145.variants.le_two {α : ℝ} (hα : α ∈ Set.Icc 0 2) : ∃ (β : ℝ), Filter.Tendsto (fun (x : ℝ) => 1 / x * ∑ n ∈ A x, (↑(s (n + 1)) - ↑(s n)) ^ α) Filter.atTop (nhds β)

Erdős [Er51] proved this for all $0\leq \alpha\leq 2$.

[Er51] Erdös, P., Some problems and results in elementary number theory. Publ. Math. Debrecen (1951), 103-109.

theorem Erdos145.erdos_145.variants.le_three {α : ℝ} (hα : α ∈ Set.Icc 0 3) : ∃ (β : ℝ), Filter.Tendsto (fun (x : ℝ) => 1 / x * ∑ n ∈ A x, (↑(s (n + 1)) - ↑(s n)) ^ α) Filter.atTop (nhds β)

Hooley [Ho73] extended this to all $\alpha\leq 3$.

[Ho73] Hooley, Christopher, On the intervals between consecutive terms of sequences. Proc. Symp. Pure Math, vol. 24, pp. 129-140. 1973.

theorem Erdos145.erdos_145.variants.le_eleven_thirds {α : ℝ} (hα : α ∈ Set.Icc 0 (11 / 3)) : ∃ (β : ℝ), Filter.Tendsto (fun (x : ℝ) => 1 / x * ∑ n ∈ A x, (↑(s (n + 1)) - ↑(s n)) ^ α) Filter.atTop (nhds β)

Greaves, Harman, and Huxley [GHH97] showed that this is true for $\alpha\leq 11/3$.

[GHH97] Greaves, G. R. H. and Harman, G. and Huxley, M. N., Sieve Methods, Exponential Sums, and their Applications in Number Theory. (1997).