Erdős problem 417 · problems.science

Let $V'(x)=\#\{\phi(m) : 1\leq m\leq x\}$ and $V(x)=\#\{\phi(m) \leq x : 1\leq m\}.$ Does $\lim V(x)/V'(x)$ exist?

Sources

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

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

417.lean

Retained formal statement1 of 2

Let $V'(x)=\#\{\phi(m) : 1\leq m\leq x\}$ and $V(x)=\#\{\phi(m) \leq x : 1\leq m\}.$ Does $\lim V(x)/V'(x)$ exist?

FormalConjectures/ErdosProblems/417.leanErdos417.erdos_417.parts.i5 linesExact file

1True ↔2  ∃ L,3    Filter.Tendsto4      (fun x => ↑{k | k ∈ Set.range Nat.totient ∧ ↑k ≤ x}.ncard / ↑(Nat.totient '' {m | 1 ≤ m ∧ ↑m ≤ x}).ncard)5      Filter.atTop (nhds L)

OpenStatement only, no proof

Sources

Search problems.science