pi_alt

@[blueprint  (title := "pi-alt")  (statement := /--    One has  $$ \pi(x) = (1+o(1)) \frac{x}{\log x}$$  as $x \to \infty$.  -/)  (proof := /--  An integration by parts gives  $$ \int_2^x \frac{dt}{\log t} = \frac{x}{\log x} - \frac{2}{\log 2} +  \int_2^x \frac{dt}{\log^2 t}.$$  We have the crude bounds  $$ \int_2^{\sqrt{x}} \frac{dt}{\log^2 t} = O( \sqrt{x} )$$  and  $$ \int_{\sqrt{x}}^x \frac{dt}{\log^2 t} = O( \frac{x}{\log^2 x} )$$  and combining all this we obtain  $$ \int_2^x \frac{dt}{\log t} = \frac{x}{\log x} + O( \frac{x}{\log^2 x} )$$  $$ = (1+o(1)) \frac{x}{\log x}$$  and the claim then follows from Theorem \ref{pi_asymp}.  -/)  (latexEnv := "corollary")]theorem pi_alt : ∃ c : ℝ → ℝ, c =o[atTop] (fun _ ↦ (1 : ℝ)) ∧    ∀ x : ℝ, Nat.primeCounting ⌊x⌋₊ = (1 + c x) * x / log x := by  obtain ⟨f, hf, h⟩ := pi_asymp  obtain ⟨f', hf', h'⟩ := integral_div_log_asymptotic  use (fun x => (log x / x) * ⌊x⌋₊.primeCounting - 1)  constructor  · apply IsLittleO.congr' (f₁ := (fun x ↦ f x + f x * f' x + f' x)) _ _ (by rfl)    · apply IsLittleO.add _ hf'      apply IsLittleO.add hf      convert! hf.mul hf'      ring    · filter_upwards [eventually_ge_atTop 2, h, h'] with x hx h h'      rw [h, intervalIntegral.integral_of_le hx, ← integral_Icc_eq_integral_Ioc, h']      have : log x ≠ 0 := by simp; grind      field  · intro x    obtain rfl|hx := eq_or_ne x 0    · simp    obtain rfl|hx := eq_or_ne x 1    · simp    obtain rfl|hx := eq_or_ne x (-1 : ℝ)    · simp      norm_num    have : log x ≠ 0 := by simp_all    field