Mertens.E₁.le

@[blueprint  "E1_bound"  (title := "Upper bound on $E_1$")  (statement := /-- One has $E_1 \leq \frac{5 \log 2 + 3}{4}$-/)  (proof := /-- We can bound $E_1 \leq \sum_{n=2}^\infty \frac{\log n}{n(n-1)} \leq \frac{\log 2}{2} + \frac{3}{2} \sum_{n=3}^\infty \frac{\log n}{n^2}$.  Calculus shows that $\log x / x^2$ is decreasing for $x \geq 2 > e^{1/2}$, so we can bound $\sum_{n=3}^\infty \frac{\log n}{n^2} \leq \int_2^\infty \frac{\log t}{t^2}\ dt = \frac{\log 2+1}{2}$.-/)  (latexEnv := "proposition")  (discussion := 1316)]theorem E₁.le : E₁ ≤ (5 * log 2 + 3) / 4 := by  unfold E₁  calc  _ = log 2 / 2 + ∑' (n : ℕ), if (n + 3).Prime then log (n + 3) / ((n + 3) * (n + 2)) else 0 := by    rw [← E₁.summable.sum_add_tsum_nat_add 3, (by rfl : range 3 = {0, 1, 2})]    simp [Nat.prime_two]    ring_nf  _ ≤ log 2 / 2 + ∑' (n : ℕ), (3 / 2) * (log (n + 3) / (n + 3) ^ 2) := by    gcongr with n    · convert! summable_nat_add_iff 3|>.mpr E₁.summable using 4      · norm_cast      · push_cast; ring    · exact summable_log_div_sq.mul_left _    · split_ifs with h      · grw [(by linarith : (n + 2 : ℝ) ≥ 2 * (n + 3) / 3)]        · field_simp          rfl        · exact log_nonneg (by grind)      · exact mul_nonneg (by norm_num) (div_nonneg (log_nonneg (by grind)) (by positivity))  _ = log 2 / 2 + (3 / 2) * ∑' (n : ℕ), log (n + 3) / (n + 3) ^ 2 := by    rw [tsum_mul_left]  _ ≤ _ := by    grw [sum_log_div_sq_le]    ring_nf    rfl