Erdős problem 145
Let be the sequence of squarefree numbers. Is it true that, for any , exists?
Sources
FormalConjectures/ErdosProblems/
145.lean
Retained formal statement
Hooley [Ho73] extended this to all .
[Ho73] Hooley, Christopher, On the intervals between consecutive terms of sequences. Proc. Symp. Pure Math, vol. 24, pp. 129-140. 1973.
∀ {α : ℝ}, α ∈ Set.Icc 0 3 → ∃ β, Filter.Tendsto (fun x => 1 / x * ∑ n ∈ Erdos145.A x, (↑(Erdos145.s (n + 1)) - ↑(Erdos145.s n)) ^ α) Filter.atTop (nhds β)SolvedStatement only, no proof