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?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/417.lean

Formal Conjectures

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

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Continue

Search problems.science