Mertens.E₂Λ.eq

@[blueprint  "Mertens-second-error-mangoldt-eq"  (title := "Integral form for second error (von Mangoldt form)")  (statement := /-- For any $x \geq 2$, one has$$ E_{2,\Lambda}(x) = \frac{E_{1,\Lambda}(x)}{\log x} - \int_x^\infty \frac{E_{1,\Lambda}(t)}{t \log^2 t}\ dt$$-/)  (proof := /--From Lemma \ref{Mertens-integral-ident} one has$$ \sum_{n \leq x} \frac{\Lambda(n)}{n \log n} = \frac{1}{\log x} \sum_{n \leq x} \frac{\Lambda(n)}{n} + \int_2^x \frac{1}{t \log^2 t} \sum_{n \leq t} \frac{\Lambda(n)}{n} \, dt.$$Now substitute the definitions of $E_{1,\Lambda}$, $E_{2,\Lambda}$, $\gamma$ and simplify.  -/)  (latexEnv := "corollary")  (discussion := 1317)]theorem E₂Λ.eq {x : ℝ} (hx : 2 ≤ x) :    E₂Λ x = E₁Λ x / log x - ∫ t in Set.Ioi x, E₁Λ t / (t * log t^2) := by  unfold E₂Λ  rw [← sum_Ioc_one_eq_sum_Ioc_zero (Nat.le_floor (by grind)) (by simp)]  conv => lhs; arg 1; arg 1; arg 2; ext n; rw [(by field : Λ n / (n * log n) = (Λ n / n) / log n)]  rw [sum_div_log_eq hx]  rw [sum_Ioc_one_eq_sum_Ioc_zero (Nat.le_floor (by grind)) (by simp), sum_mangoldt_div_eq]  have : ∫ t in 2..x, (∑ n ∈ Ioc 1 ⌊t⌋₊, Λ n / n) / (t * log t ^ 2) = ∫ t in 2..x, (1 / (t * log t) + E₁Λ t / (t * log t ^ 2)) := by    refine intervalIntegral.integral_congr fun t ht ↦ ?_    rw [Set.uIcc_of_le hx, Set.mem_Icc] at ht    rw [sum_Ioc_one_eq_sum_Ioc_zero (Nat.le_floor (by grind)) (by simp), sum_mangoldt_div_eq]    field  rw [this, intervalIntegral.integral_add]  · rw [integral_one_div_mul_log hx, add_div, div_self (by simp; grind)]    unfold γ    calc    _ = E₁Λ x / log x + (∫ (x : ℝ) in 2..x, E₁Λ x / (x * log x ^ 2)) -      ((∫ (t : ℝ) in Set.Ioi 2, E₁Λ t / (t * log t ^ 2))) := by ring    _ = _ := by      rw [← intervalIntegral.integral_interval_add_Ioi (integrable_E₁Λ_div_mul_log_sq (by rfl)) (integrable_E₁Λ_div_mul_log_sq hx)]      ring  · exact intervalIntegrable_one_div_mul_log hx  · rw [intervalIntegrable_iff, Set.uIoc_of_le hx]    exact integrable_E₁Λ_div_mul_log_sq (x := 2) (by rfl)|>.mono (by grind) (by rfl)