Erdos392.tendsto_primeCounting_div_id_zero

lemma tendsto_primeCounting_div_id_zero :    Filter.Tendsto (fun n ↦ (Nat.primeCounting n : ℝ) / n) .atTop (nhds 0) := by  have h_upper_bound : ∀ n : ℕ, 2 ≤ n →      (primeCounting n : ℝ) / n ≤        Real.sqrt n / n + (2 * Real.log 4) / Real.log n := by    intro n hn    rw [div_le_iff₀ (by positivity)]    convert! primeCounting_le_bound n hn using 1    · ring_nf; norm_num [show n ≠ 0 by positivity]  have h_tendsto : Filter.Tendsto      (fun n : ℕ ↦ .sqrt n / n + (2 * Real.log 4) / Real.log n)      .atTop (nhds 0) := by    have h1 : Filter.Tendsto (fun n : ℕ ↦ Real.sqrt n / n) .atTop (nhds 0) := by      simpa [sqrt_div_self] using tendsto_inv_atTop_nhds_zero_nat.sqrt    have h2 : Filter.Tendsto (fun n : ℕ ↦ (2 * Real.log 4) / Real.log n) .atTop (nhds 0) :=      tendsto_const_nhds.div_atTop (tendsto_log_atTop.comp tendsto_natCast_atTop_atTop)    simpa using h1.add h2  exact squeeze_zero_norm' (Filter.eventually_atTop.mpr ⟨2, fun n hn ↦ by    rw [norm_of_nonneg (by positivity)]; exact h_upper_bound n hn⟩) h_tendsto