Erdős problem 416
Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. V(x)=x/logx * e^((C+o(1))(log log log x)^2), for some explicit constant C>0. Ref:Maier, Helmut and Pomerance, Carl, _On the number of distinct values of Euler's -function_.
Sources
FormalConjectures/ErdosProblems/
416.lean
Retained formal statement
Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. Pillai proved V(x)=o(x). Ref: S. Sivasankaranarayana Pillai, _On some functions connected with _
Erdos416.V =o[Filter.atTop] idSolvedStatement only, no proof