Ramanujan.pi_error_identity

@[blueprint  "pi-error-identity"  (title := "Integral identity for pi - Li")  (statement := /-- If $x \geq 2$, then$$\pi(x) - \textrm{Li}(x) = \frac{\theta(x) - x}{\log x} + \frac{2}{\log 2} + \int_{2}^{x} \frac{\theta(t) -t}{t \log^{2}t}\, dt.$$ -/)  (proof := /-- Follows from Sublemma \ref{rs-417} and the fundamental theorem of calculus. -/)  (latexEnv := "lemma")  (discussion := 986)]theorem pi_error_identity (x : ℝ) (hx : 2 ≤ x) :    pi x - Li x = (θ x - x) / log x + 2 / log 2 + ∫ t in Icc 2 x, (θ t - t) / (t * log t ^ 2) := by  have h_integral : ∫ t in Set.Icc 2 x, (θ t - t) / (t * log t ^ 2) =      (∫ t in Set.Icc 2 x, θ t / (t * log t ^ 2)) -      (∫ t in Set.Icc 2 x, 1 / log t ^ 2) := by    rw [← MeasureTheory.integral_sub]    · exact MeasureTheory.setIntegral_congr_fun measurableSet_Icc fun t ht ↦ by        rw [sub_div, div_eq_mul_inv]; ring_nf        norm_num [show t ≠ 0 by linarith [ht.1], show log t ≠ 0 from ne_of_gt <| log_pos <| by linarith [ht.1]]    · have h_bound : ∀ t ∈ Set.Icc 2 x, |θ t / (t * log t ^ 2)| ≤ log 4 / log t ^ 2 := by        intro t ht        have : θ t ≤ log 4 * t := Chebyshev.theta_le_log4_mul_x (by linarith [ht.1])        rw [abs_of_nonneg (div_nonneg (by exact Finset.sum_nonneg fun _ _ ↦              log_nonneg <| Nat.one_le_cast.2 <| Nat.Prime.pos <| by aesop)            (mul_nonneg (by linarith [ht.1]) (sq_nonneg _))), div_le_div_iff₀] <;>          nlinarith [ht.1, ht.2, log_pos <| show 1 < t by linarith [ht.1],            log_le_sub_one_of_pos <| show 0 < t by linarith [ht.1],            show 0 ≤ θ t from Finset.sum_nonneg fun _ _ ↦              log_nonneg <| Nat.one_le_cast.2 <| Nat.Prime.pos <| by aesop]      refine MeasureTheory.Integrable.mono' (g := fun t ↦ log 4 / log t ^ 2) ?_ ?_ ?_      · exact ContinuousOn.integrableOn_Icc (continuousOn_of_forall_continuousAt fun t ht ↦          ContinuousAt.div continuousAt_const            (ContinuousAt.pow (continuousAt_log (by linarith [ht.1])) _)              (ne_of_gt (sq_pos_of_pos (log_pos (by linarith [ht.1])))))      · refine (Measurable.mul ?_ ?_).aestronglyMeasurable        · have : Measurable (fun t : ℕ ↦ ∑ p ∈ Finset.filter Nat.Prime (Finset.Icc 0 t), log p) :=            measurable_from_nat          exact this.comp measurable_id'.nat_floor        · exact Measurable.inv (measurable_id.mul (measurable_log.pow_const 2))      · filter_upwards [MeasureTheory.ae_restrict_mem measurableSet_Icc] with t ht using h_bound t ht    · exact ContinuousOn.integrableOn_Icc (continuousOn_const.div        (ContinuousOn.pow (continuousOn_log.mono <| by norm_num) _) fun t ht ↦        ne_of_gt <| sq_pos_of_pos <| log_pos <| by linarith [ht.1])  have h_pi : pi x = θ x / log x + ∫ t in Icc 2 x, θ t / (t * log t ^ 2) := by    rw [integral_Icc_eq_integral_Ioc, ← intervalIntegral.integral_of_le hx]    exact primeCounting_eq_theta_div_log_add_integral hx  rw [h_integral, h_pi, Li_eq_sub_add_integral x hx]; ring