Erdős problem 416 · problems.science

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 $\phi$ -function_.

Sources

Browse retained paths and inspect the exact material available for this Problem.

6 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

416.lean

Retained formal statement4 of 6

Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. V(x) ≍ x/log x*e^(C_1*(log log log x − log log log log x)^2+C_2 log log log x − C_3 log log log log x) Ref: Ford, Kevin, _The distribution of totients_.

FormalConjectures/ErdosProblems/416.leanErdos416.erdos_416.variants.Ford12 linesExact file

1match sorry with2| (C₁, C₂, C₃) =>3  0 < C₁ ∧4    0 < C₂ ∧5      0 < C₃ ∧6        have G := fun x =>7          x / Real.log x *8            Real.exp9              (C₁ * (Real.log (Real.log (Real.log x)) - Real.log (Real.log (Real.log (Real.log x)))) ^ 2 +10                  C₂ * Real.log (Real.log (Real.log x)) -11                C₃ * Real.log (Real.log (Real.log (Real.log x))));12        Erdos416.V =Θ[Filter.atTop] G

SolvedStatement only, no proof

Sources

Search problems.science