Erdős problem 358
When , the function defined above counts the number of odd divisors of .
Sources
FormalConjectures/ErdosProblems/
358.lean
Retained formal statement
Let be an infinite sequence of integers. Let count the number of solutions to Is there such an for which as ?
Tao [Ta26] constructed such a sequence with for all sufficiently large .
True ↔ ∃ A, StrictMono A ∧ Filter.Tendsto (Erdos358.f A) Filter.atTop Filter.atTopSolvedStatement only, no proof