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. 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_.
have C := sorry;0 < C ∧ ∃ f, f =o[Filter.atTop] 1 ∧ ∀ᶠ (x : ℝ) in Filter.atTop, Erdos416.V x = x / Real.log x * Real.exp ((C + f x) * Real.log (Real.log (Real.log x)) ^ 2)SolvedStatement only, no proof