Erdős problem 410
Let , the sum of divisors function, and .
Sources
FormalConjectures/ErdosProblems/
410.lean
Retained formal statement
Let , the sum of divisors function, and .
Is it true that ?
This is problem (iii) from Erdos, Granville, Pomerance, Spiro "On the normal behavior of the iterates of some arithmetical functions" (page 169 of the book "Analytic Number Theory", 1990).
True ↔ ∀ n > 1, Filter.Tendsto (fun k => ↑((⇑(ArithmeticFunction.sigma 1))^[k] n) ^ (1 / ↑k)) Filter.atTop Filter.atTopOpenStatement only, no proof