Mertens.E₁Λ.ge

@[blueprint  "Mertens-first-error-mangoldt-ge"  (title := "Partial sum of $\\Lambda(d)/d$ lower bound")  (statement := /-- For any $x \geq 1$, one has$$ E_{1,\Lambda}(x) \geq - 2.$$-/)  (proof := /-- Insert Lemma \ref{Mertens-sum-log-eq-sum-mangoldt} into Lemma \ref{Mertens-sum-log-ge} and lower bound $x/d$ by $\lfloor x/d \rfloor$.  -/)  (latexEnv := "corollary")  (discussion := 1307)]theorem E₁Λ.ge {x : ℝ} (hx : 1 ≤ x) :    E₁Λ x  ≥ -2 := by  unfold E₁Λ  suffices x * ∑ d ∈ Ioc 0 ⌊x⌋₊, Λ d / d  ≥ x * (log x - 2) 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⌋₊ := by    gcongr    exact Nat.floor_le <| div_nonneg (by linarith) (by linarith)  _ ≥ x * log x - 2 * x :=    sum_log_eq_sum_mangoldt ▸ sum_log_ge hx  _ = _ := by ring