feat(Mertens): prove log_zeta_eq_integ via Abel summation (#1583)

[giuseppesorge]

Closes #1583.

Proves log_zeta_eq_integ (integration-by-parts identity): for real $s>1$,
$\log\zeta(s) = (s-1)\int_1^\infty (\log\log x + \gamma + E_{2,\Lambda}(x)),x^{-s},dx$.

Route (Abel summation): the integrand equals the summatory function $\sum_{d\le x}\Lambda(d)/(d\log d)$ (by the definition of $E_{2,\Lambda}$), and the sum/integral interchange (MeasureTheory.integral_tsum_of_summable_integral_norm, all terms $\ge 0$) with $\int_d^\infty x^{-s},dx = d^{1-s}/(s-1)$ (integral_Ioi_rpow_of_lt) gives $(s-1)\int = \sum_d \Lambda(d)/(d^s\log d) = \log\zeta(s)$ via log_zeta_eq_sum (#1582). Helpers are in a private sub-namespace Mertens.LogZetaInteg.

Note (blueprint DAG): log_zeta_eq_integ transitively depends on log_zeta_eq_sum (#1582), still sorry on main (my PR #1595). The interchange/Abel-summation argument and all helper lemmas here are complete and axiom-clean. No new imports. Full project builds (lake build, 4187 jobs).

[teorth]

This proof is lengthier than expected, which will likely cause problems with the eventual upstreaming to Mathlib. It's possible that a general summability lemma, to the effect that any series bounded in magnitude by O( log^a n / n^s ) for some real a and s > 1, would be worth developing here in order to handle all the various summability conditions needed.

[giuseppesorge]

Thanks — I've added the general summability majorant you suggested.

summable_log_rpow_div_rpow (a : ℝ) {s : ℝ} (hs : 1 < s) : Summable (fun n : ℕ => (log n)^a / n^s)

proved from isLittleO_log_rpow_rpow_atTop (so (log n)^a = o(n^ε)) plus summable_of_isBigO_nat. Both summability conditions in this node now reduce to it:

• summable_vonMangoldt_div_rpow (Λ n / n^s) is just domination by log n / n^s via vonMangoldt_le_log (a = 1) — replacing the previous LSeriesSummable_vonMangoldt/LSeries.term unfolding.
• summable_c_term collapses to a plain p-series once the log d in c d = Λ d/(d log d) cancels against Λ d ≤ log d.

Net it's only marginally shorter, but the two conditions now read as "dominated by the general majorant" rather than ad-hoc rpow manipulation, which should travel better to Mathlib. The majorant is reusable for the other nodes' summability conditions too. Let me know if you'd prefer a different form (e.g. an IsBigO-stated comparison wrapper).

[giuseppesorge]

Small correction to the above: in the pushed version summable_c_term reduces to summable_vonMangoldt_div_rpow (majorised by (1/(log 2·(s-1)))·Λ d/d^s) rather than directly to a p-series — this keeps the general summable_log_rpow_div_rpow lemma genuinely on the proof path (used at a = 1). Net effect on the conditions is the same.