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
Let be the sequence of squarefree numbers. Is it true that, for any , exists?
True ↔ ∀ α ≥ 0, ∃ β, Filter.Tendsto (fun x => 1 / x * ∑ n ∈ Erdos145.A x, (↑(Erdos145.s (n + 1)) - ↑(Erdos145.s n)) ^ α) Filter.atTop (nhds β)OpenStatement only, no proof