Skip to content

Erdős problem 416

Start work

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

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

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−1p-1 and some related problems concerning Euler's φ\varphi-function._

FormalConjectures/ErdosProblems/416.leanErdos416.erdos_416.variants.Erdos1 lineExact file
∃ f, f =o[Filter.atTop] 1 ∧ ∀ᶠ (x : ℝ) in Filter.atTop, Erdos416.V x = x * Real.log x ^ (-1 + f x)
SolvedStatement only, no proof