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 statement3 of 6

Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. Erdős proved V(x)=x(logx)^(−1+o(1)). Ref: Erdős, P., _On the normal number of prime factors of $p-1$ and some related problems concerning Euler's $\varphi$ -function._

FormalConjectures/ErdosProblems/416.leanErdos416.erdos_416.variants.Erdos1 lineExact file

1∃ f, f =o[Filter.atTop] 1 ∧ ∀ᶠ (x : ℝ) in Filter.atTop, Erdos416.V x = x * Real.log x ^ (-1 + f x)

SolvedStatement only, no proof

Sources

Search problems.science