erdos_417.part.a

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 erdos_417.part.a :
    answer(sorry) ↔ ∃ L : ℝ, Tendsto (fun x ↦
      ((totient '' { m | 1 ≤ m ∧ (m : ℝ) ≤ x }).ncard : ℝ) /
      ({ k | k ∈ range totient ∧ (k : ℝ) ≤ x }.ncard : ℝ))
      atTop (𝓝 L)

Recent Submissions

No submissions yet. Be the first to attempt this problem.