Mertens.E₁Λ.le

@[blueprint  "Mertens-first-error-mangoldt-le"  (title := "Partial sum of $\\Lambda(d)/d$ upper bound")  (statement := /-- For any $x \geq 1$, one has$$ E_{1,\Lambda}(x) \leq \log 4 + 4.$$-/)  (proof := /-- Insert Lemma \ref{Mertens-sum-log-eq-sum-mangoldt} into Lemma \ref{Mertens-sum-log-le} and upper bound $x/d$ by $\lfloor x/d \rfloor + 1$, and use the Mathlib bound $\psi(x) \leq (\log 4 + 4) x$.  -/)  (latexEnv := "corollary")  (discussion := 1308)]theorem E₁Λ.le {x : ℝ} (hx : 1 ≤ x) :    E₁Λ x ≤ log 4 + 4 := by  unfold E₁Λ  suffices x * ∑ d ∈ Ioc 0 ⌊x⌋₊, Λ d / d ≤ x * (log x + log 4 + 4) by    linarith [le_of_mul_le_mul_left this (by linarith)]  calc  _ = ∑ d ∈ Ioc 0 ⌊x⌋₊, Λ d * (x / d) := by    rw [Finset.mul_sum]    ring_nf  _ ≤ ∑ d ∈ Ioc 0 ⌊x⌋₊, Λ d * (⌊x / d⌋₊ + 1) := by    gcongr    exact Nat.lt_floor_add_one _|>.le  _ = (∑ d ∈ Ioc 0 ⌊x⌋₊, log d) + ∑ d ∈ Ioc 0 ⌊x⌋₊, Λ d := by    simp_rw [mul_add, mul_one]    rw [Finset.sum_add_distrib, sum_log_eq_sum_mangoldt]  _ ≤ x * log x + (log 4 + 4) * x := by    gcongr    · exact sum_log_le hx    · exact Chebyshev.psi_le_const_mul_self (by linarith)  _ = _ := by ring