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
Erdős [Er51] proved this for all .
[Er51] Erdös, P., Some problems and results in elementary number theory. Publ. Math. Debrecen (1951), 103-109.
∀ {α : ℝ}, α ∈ Set.Icc 0 2 → ∃ β, Filter.Tendsto (fun x => 1 / x * ∑ n ∈ Erdos145.A x, (↑(Erdos145.s (n + 1)) - ↑(Erdos145.s n)) ^ α) Filter.atTop (nhds β)SolvedStatement only, no proof