norm_eulerPrimeLogDerivTermComplex_le_carrierDerivTerm
plain-language theorem explainer
The per-prime complex log-derivative term arising from the Euler product is bounded in norm by the real carrier derivative term evaluated at Re(s). Analysts lifting real summability results to the complex strip for zeta-function estimates would cite this domination. The proof is a direct calc that applies the norm inequality for the complex term and the equality identifying the resulting expression with carrierDerivTerm.
Claim. For complex $s$ with $0 < {Re}(s)$ and prime $p$, the norm of the complex per-prime logarithmic derivative contribution $({log} p) p^{-2s}/(1-p^{-s})$ satisfies $|| (log p) p^{-2s}/(1-p^{-s}) || ≤ p^{-2σ} (log p)/(1-p^{-σ})$ where $σ = {Re}(s)$.
background
The EulerInstantiation module instantiates the abstract RS carrier/sensor framework by realizing the Euler product of ζ(s) as a concrete carrier. carrierDerivTerm(p, σ) is the per-prime term p^{-2σ} log p / (1 - p^{-σ}) that appears in the logarithmic derivative bound M_C(σ₀) = 2 ∑_p carrierDerivTerm(p, σ₀). eulerPrimeLogDerivTermComplex(p, s) is the complex analogue ((log p) (p^{-s})^2) / (1 - p^{-s}), obtained by substituting the complex power p^{-s} = exp(-s log p). The upstream result norm_eulerPrimeLogDerivTermComplex_le supplies the intermediate norm bound primeLog p · ||p^{-s}||² / (1 - ||p^{-s}||) under the hypothesis 0 < Re(s).
proof idea
The term-mode proof is a two-step calc. The first step invokes norm_eulerPrimeLogDerivTermComplex_le to replace the left-hand norm by primeLog p · ||eulerPrimePowerComplex p s||² / (1 - ||eulerPrimePowerComplex p s||). The second step applies norm_form_eq_carrierDerivTerm to equate that expression exactly to carrierDerivTerm p s.re.
why it matters
The bound is invoked inside eulerPrimeLogDerivTermComplex_summable to dominate the complex series by the real summable series carrierDerivBound_summable, thereby lifting the real convergence result to Re(s) > 1/2. This step completes the passage from the real carrier derivative bound to the complex EulerCarrier interface required for the cost-covering axiom and the conditional Riemann hypothesis. It sits inside the module's chain primes → Hilbert–Schmidt norm → det₂ convergence → logarithmic derivative bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.