Erdos392.primeCounting_is_o_id

@[blueprint  "primeCounting-is-o-id"  (statement := /-- $$\pi(n) = o(n) \quad \text{as } n \to \infty.$$ -/)  (proof := /-- Given $\varepsilon > 0$, choose $a \neq 0$ with $\varphi(a)/a < \varepsilon/2$(using $\prod_{p \leq n}(1 - 1/p) \to 0$). For $n \geq a + 2$,$$\pi(n) \leq \frac{\varphi(a)}{a} \cdot n + \varphi(a) + \pi(a+1) + 1.$$Since $\varphi(a)/a < \varepsilon/2$, for $n$ large enough the constant terms are absorbed,giving $\pi(n) < \varepsilon n$. -/)  (latexEnv := "lemma")]lemma primeCounting_is_o_id :    IsLittleO .atTop (fun n ↦ (primeCounting n : ℝ)) (fun n ↦ (n : ℝ)) := by  refine isLittleO_iff.mpr fun ε hε ↦ ?_  obtain ⟨a, ha_ne_zero, ha_bound⟩ : ∃ a : ℕ, a ≠ 0 ∧ (a.totient : ℝ) / a < ε / 2 :=    exists_phi_div_self_lt (half_pos hε)  obtain ⟨N, hN⟩ : ∃ N : ℕ, ∀ n ≥ N,      (primeCounting' n : ℝ) ≤        (a.totient : ℝ) / a * n + (a.totient : ℝ) +        primeCounting' (a + 1) := by    refine ⟨a + 1 + 1, fun n hn ↦ ?_⟩    have := primeCounting'_add_le ha_ne_zero (lt_succ_self a) (n - (a + 1))    simp only [ne_eq, ge_iff_le, primeCounting'] at *    rw [div_mul_eq_mul_div, div_add', div_add', le_div_iff₀] <;> norm_cast <;> try positivity    rw [show a + 1 + (n - (a + 1)) = n by rw [add_tsub_cancel_of_le (by linarith)]] at this    nlinarith [Nat.zero_le (φ a), Nat.zero_le (count Nat.Prime (a + 1)),      Nat.zero_le ((n - (a + 1)) / a), Nat.div_mul_le_self (n - (a + 1)) a,      Nat.sub_add_cancel (by linarith : a + 1 ≤ n)]  have hN_primeCounting : ∀ᶠ n in .atTop, (primeCounting n : ℝ) ≤      (totient a : ℝ) / a * (n : ℝ) + (totient a : ℝ) + primeCounting' (a + 1) + 1 := by    simp only [ne_eq, ge_iff_le, primeCounting', primeCounting, Filter.eventually_atTop] at *    refine ⟨N + 1, fun b hb ↦ ?_⟩    specialize hN (b + 1) (by linarith)    simp_all only [count_succ, cast_add, cast_ite, cast_one, CharP.cast_eq_zero]    have h_phi_le : (φ a : ℝ) / a ≤ 1 := by      rw [div_le_iff₀ (cast_pos.mpr <| pos_of_ne_zero ha_ne_zero)]      simp [one_mul, totient_le a]    nlinarith  norm_num at *  obtain ⟨M, hM⟩ := hN_primeCounting  let C := (φ a : ℝ) + primeCounting' (a + 1) + 1  refine ⟨M + ⌈C / (ε / 2)⌉₊ + 1, fun n hn ↦ ?_⟩  have h_ceil := le_ceil (C / (ε / 2))  have h_cancel := mul_div_cancel₀ C (by positivity : ε / 2 ≠ 0)  have h_n_ge : (n : ℝ) ≥ M + ⌈C / (ε / 2)⌉₊ + 1 := by exact_mod_cast hn  nlinarith [hM n (by linarith)]