Mertens.E₁Λ.le_E₁p_add_E₁

@[blueprint  "Mertens-first-error-prime-ge"  (title := "Partial sum of $\\frac{\\log p}{p}$ lower bound")  (statement := /-- For any $x \geq 1$, one has$$ E_{1,\Lambda}(x) \leq E_{1,p}(x) + E_1$$and thus$$ E_{1,p}(x) \geq -2 - E_1$$where$$ E_1 := \sum_{p} \frac{\log p}{p(p-1)}. $$-/)  (proof := /-- Use the triangle inequality and the geometric series formula to estimate in Lemma \ref{Mertens-sum-mangoldt-div-le} arising from prime powers.  -/)  (latexEnv := "corollary")  (discussion := 1312)]theorem E₁Λ.le_E₁p_add_E₁ {x : ℝ} (hx : 1 ≤ x) :    E₁Λ x ≤ E₁p x + E₁ := by  unfold E₁Λ E₁p  suffices ∑ d ∈ Ioc 0 ⌊x⌋₊, Λ d / d ≤ ∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, log p / p + E₁ by linarith  simp_rw [vonMangoldt_apply, ite_div, zero_div, ← sum_filter, Chebyshev.sum_PrimePow_eq_sum_sum _ (by linarith)]  calc  _ = ∑ k ∈ Icc 1 ⌊log x / log 2⌋₊, ∑ p ∈ Ioc 0 ⌊x ^ (1 / (k : ℝ))⌋₊ with Nat.Prime p, log p / (p ^ k : ℕ) := by    refine sum_congr rfl fun k hk ↦ sum_congr rfl fun p hp ↦ ?_    rw [Nat.Prime.pow_minFac (by simp_all) (by simp_all; linarith)]  _ ≤ ∑ k ∈ Icc 1 ⌊log x / log 2⌋₊, ∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, log p / (p ^ k : ℕ) := by    gcongr with k hk    apply rpow_le_self_of_one_le hx    simp only [mem_Icc] at hk    exact div_le_one₀ (by norm_cast; linarith)|>.mpr (mod_cast hk.1)  _ ≤ ∑ k ∈ Icc 1 (max 1 ⌊log x / log 2⌋₊), ∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, log p / (p ^ k : ℕ) := by    apply sum_le_sum_of_subset_of_nonneg    · gcongr      exact le_max_right ..    · exact fun _ _ _ ↦ sum_nonneg fun _ _ ↦ (by positivity)  _ = ∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, (log p / p) + ∑ k ∈ Ioc 1 (max 1 ⌊log x / log 2⌋₊), ∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, log p / (p ^ k : ℕ) := by    rw [← add_sum_Ioc_eq_sum_Icc (le_max_left ..)]    simp  _ ≤ _ := by    gcongr    rw [sum_comm]    conv => lhs; arg 2; ext p; arg 2; ext k; rw [← mul_one_div, Nat.cast_pow, ← one_div_pow]    simp_rw [← mul_sum]    calc    _ ≤ ∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, log p / (p * (p - 1)) := by      gcongr with p hp      simp only [mem_filter, mem_Ioc] at hp      conv => rhs; rw [← mul_one_div]      gcongr      rw [(by rfl : Ioc 1 (max 1 ⌊log x / log 2⌋₊) = Ico 2 (max 1 ⌊log x / log 2⌋₊  + 1))]      grw [geom_sum_Ico_le_of_lt_one (by simp)]      · apply le_of_eq        have : (p : ℝ) ≠ 0 := by exact_mod_cast hp.1.1.ne.symm        field      · simpa using inv_lt_one_of_one_lt₀ (mod_cast hp.2.one_lt)    _ ≤ _ := by      rw [sum_filter]      exact E₁.summable.sum_le_tsum _ fun p hp ↦ E₁.summand_nonneg p