Zeta--von Mangoldt bridge for Mertens constants

This module begins the constant-identification workline. It records the analytic normalization at s = 1; connecting it to hard prime cutoffs is the remaining Abelian bridge.

theorem AnalyticNumberTheory.Mertens.zeta_log_vonMangoldt_isBigO : (fun (s : ℝ) => ∑' (n : ℕ), ArithmeticFunction.vonMangoldt n / (↑n ^ s * Real.log ↑n) + Real.log (s - 1)) =O[nhdsWithin 1 (Set.Ioi 1)] fun (s : ℝ) => s - 1

The logarithm of zeta, expressed through the von Mangoldt Dirichlet series, has the standard normalized O(s - 1) behavior at 1 from the right.

theorem AnalyticNumberTheory.Mertens.zeta_euler_log_eq_LSeries {s : ℂ} (hs : 1 < s.re) : ∑' (p : Nat.Primes), -Complex.log (1 - 1 ↑↑p * ↑↑p ^ (-s)) = LSeries (fun (n : ℕ) => 1 ↑n * ↑(ArithmeticFunction.vonMangoldt n) / ↑(Real.log ↑n)) s

The prime Euler-log expansion of the zeta logarithm. This is the analytic prime-side counterpart of the finite product bridge.

theorem AnalyticNumberTheory.Mertens.summable_zeta_primeEulerLog {s : ℂ} (hs : 1 < s.re) : Summable fun (p : Nat.Primes) => -Complex.log (1 - 1 ↑↑p * ↑↑p ^ (-s))

Above the line of absolute convergence, the prime Euler-log series is summable.

theorem AnalyticNumberTheory.Mertens.summable_zeta_primeDirichlet {s : ℂ} (hs : 1 < s.re) : Summable fun (p : Nat.Primes) => ↑↑p ^ (-s)

The prime Dirichlet series is summable in the half-plane Re(s) > 1.

theorem AnalyticNumberTheory.Mertens.summable_zeta_primeEulerCorrection {s : ℂ} (hs : 1 < s.re) : Summable fun (p : Nat.Primes) => -Complex.log (1 - ↑↑p ^ (-s)) - ↑↑p ^ (-s)

The quadratic-and-higher analytic correction is summable above Re(s)=1.

theorem AnalyticNumberTheory.Mertens.primeEulerLog_tsum_decomposition {s : ℂ} (hprime : Summable fun (p : Nat.Primes) => ↑↑p ^ (-s)) (hcorrection : Summable fun (p : Nat.Primes) => -Complex.log (1 - ↑↑p ^ (-s)) - ↑↑p ^ (-s)) : ∑' (p : Nat.Primes), -Complex.log (1 - ↑↑p ^ (-s)) = ∑' (p : Nat.Primes), ↑↑p ^ (-s) + ∑' (p : Nat.Primes), (-Complex.log (1 - ↑↑p ^ (-s)) - ↑↑p ^ (-s))

Algebraic decomposition of the Euler-log summand into its prime Dirichlet term and its quadratic-and-higher correction. Summability is kept explicit: establishing it uniformly as s → 1⁺ is part of the Abelian workline.

theorem AnalyticNumberTheory.Mertens.zeta_primeEulerLog_decomposition {s : ℂ} (hs : 1 < s.re) : ∑' (p : Nat.Primes), -Complex.log (1 - ↑↑p ^ (-s)) = ∑' (p : Nat.Primes), ↑↑p ^ (-s) + ∑' (p : Nat.Primes), (-Complex.log (1 - ↑↑p ^ (-s)) - ↑↑p ^ (-s))

Unconditional Euler-log decomposition in the half-plane of absolute convergence.

theorem AnalyticNumberTheory.Mertens.real_primeEulerLog_eq_log_riemannZeta {s : ℝ} (hs : 1 < s) : ∑' (p : Nat.Primes), -Real.log (1 - ↑↑p ^ (-s)) = Real.log (riemannZeta ↑s).re

Real specialization of the prime Euler-log expansion. This is the normalization interface used by the Abelian finite-part argument at s = 1.