RS_prime.pnt

@[blueprint  "rs-pnt"  (title := "A medium version of the prime number theorem")  (statement := /-- $\vartheta(x) = x + O( x / \log^2 x)$. -/)  (proof := /-- This in principle follows by establishing an analogue of Theorem \ref{chebyshev-asymptotic}, using mediumPNT in place of weakPNT. -/)  (latexEnv := "theorem")  (discussion := 597)]theorem pnt : ∃ C ≥ 0, ∀ x ≥ 2, |θ x - x| ≤ C * x / log x ^ 2 := by  obtain ⟨c, hc⟩ := isBigO_iff'.1 pntBigO  obtain ⟨N, hN⟩ := eventually_atTop.1 hc.2  by_cases! hn : 2 ≤ N  · refine ⟨max c (4 * (θ N + N)), le_max_of_le_left hc.1.le, fun x hx => ?_⟩    by_cases! h : x ≤ N    · suffices |θ x - x| * log x ^ 2 / x ≤ 4 * (θ N + N) from by        rw [le_div_iff₀ (sq_pos_of_pos (log_pos (by linarith))), ← div_le_iff₀ (by linarith)]        exact this.trans (le_max_right c (4 * (θ N + N)))      have : |θ x - x| ≤ θ N + N := calc        _ ≤ |θ x| + |x| := abs_sub _ _        _ = θ x + x := by rw [abs_of_nonneg (theta_nonneg _), abs_of_nonneg (by linarith)]        _ ≤ _ := by gcongr      calc      _ ≤ (θ N + N) * log x ^ 2 / x := by gcongr      _ ≤ (θ N + N) * (x ^ (1 / 2 : ℝ) / (1 / 2)) ^ 2 / x := by        gcongr        · exact log_nonneg (by linarith)        · exact log_le_rpow_div (by linarith) (by linarith)      _ = _ := by rw [← sqrt_eq_rpow, div_pow, sq_sqrt (by linarith)]; field_simp; ring    · simpa [abs_of_nonneg (by grind : 0 ≤ x), mul_div] using (hN x h.le).trans <|        mul_le_mul_of_nonneg_right (le_max_left c (4 * (θ N + N))) (norm_nonneg _)  · refine ⟨c, hc.1.le, fun x hx => ?_⟩    simpa [abs_of_nonneg (by grind : 0 ≤ x), mul_div] using hN x (hn.le.trans hx)