Erdős Problem 208

Reference: erdosproblems.com/208

noncomputable def Erdos208.erdos208.s : ℕ → ℕ

The sequence of squarefree numbers, denoted by s as in Erdős problem 208.

Equations

• Erdos208.erdos208.s = Nat.nth Squarefree

theorem Erdos208.erdos_208.i : (∀ ε > 0, (fun (n : ℕ) => ↑(erdos208.s (n + 1)) - ↑(erdos208.s n)) =O[Filter.atTop] fun (n : ℕ) => ↑(erdos208.s n) ^ ε) ↔ sorry

Let $s_1 < s_2 < ⋯$ be the sequence of squarefree numbers. Is it true that for any $ϵ > 0$ and large $n$, $s_{n+1} − s_n ≪_ϵ s_n^ε$?

theorem Erdos208.erdos_208.ii : (∃ (c : ℕ → ℝ), c =o[Filter.atTop] 1 ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(erdos208.s (n + 1)) - ↑(erdos208.s n) ≤ (1 + c n) * (Real.pi ^ 2 / 6) * Real.log ↑(erdos208.s n) / Real.log (Real.log ↑(erdos208.s n))) ↔ sorry

Let $s_1 < s_2 < ⋯$ be the sequence of squarefree numbers. Is it true that $s_{n + 1} - s_n ≤ (1 + o(1)) * (\pi^2 / 6) * log (s_n) / log (log (s_n))$?

theorem Erdos208.erdos_208.variants.log_bound : (fun (n : ℕ) => ↑(erdos208.s (n + 1)) - ↑(erdos208.s n)) =O[Filter.atTop] fun (n : ℕ) => Real.log ↑(erdos208.s n)

In [Er79] Erdős says perhaps $s_{n+1} − s_n ≪ log s_n$, but he is 'very doubtful'.

[Er79] Erdős, Paul, Some unconventional problems in number theory. Math. Mag. (1979), 67-70.