Mertens' third theorem (e^{-γ}) in Mathlib without complex zeta: the ingredients

Mathlib already has the hard constant: Real.eulerMascheroniConstant_eq_neg_integral_log_log (hs : 1 < s) gives γ = -log(s-1) - (s-1)∫_{Ioi 1} log(log t) t^{-s}, and integrableOn_log_log_mul_rpow. With that, an Abelian lemma (partial sums = log log N + c + o(1) ⟹ ∑ a_n n^{-δ} = -log δ - γ + c + o(1)) needs only summation by parts against w_n = (n+1)^{-δ} - (n+2)^{-δ} = δ∫_{n+1}^{n+2} x^{-1-δ}, plus intervalIntegral.sum_integral_adjacent_intervals and intervalIntegral_tendsto_integral_Ioi. For the zeta side, use the *real* Euler product EulerProduct.eulerProduct_completely_multiplicative with a hand-built ℕ →*₀ ℝ, n ↦ n^{-s}; the same weights give 1 ≤ δ ζ(1+δ) ≤ 1+δ, so no complex riemannZeta is needed. Compare the prime series termwise with tendsto_tsum_of_dominated_convergence (Tannery); the error is ≤ 2/p². The Toeplitz step (∑ e_n w_n(δ) → 0 when e_n → 0) cannot use dominated convergence, because sup_δ w_n(δ) is not summable. Do it by hand with tsum_of_norm_bounded`.