Erdős Problem 417

References:

• erdosproblems.com/417
• [Er98] Erdős, Paul, Some of my new and almost new problems and results in combinatorial number theory. Number theory (Eger, 1996) (1998), 169-180.

theorem Erdos417.erdos_417.part.a : sorry ↔ ∃ (L : ℝ), Filter.Tendsto (fun (x : ℝ) => ↑(Nat.totient '' {m : ℕ | 1 ≤ m ∧ ↑m ≤ x}).ncard / ↑{k : ℕ | k ∈ Set.range Nat.totient ∧ ↑k ≤ x}.ncard) Filter.atTop (nhds L)

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?

Formalization note: We formalize the limit of the inverse fraction V'(x)/V(x) to ensure the limit is finite (bounded between 0 and 1).

theorem Erdos417.erdos_417.part.b : sorry ↔ ∃ L < 1, Filter.Tendsto (fun (x : ℝ) => ↑(Nat.totient '' {m : ℕ | 1 ≤ m ∧ ↑m ≤ x}).ncard / ↑{k : ℕ | k ∈ Set.range Nat.totient ∧ ↑k ≤ x}.ncard) Filter.atTop (nhds L)

Is it $>1$?