10 Cesàro Regularization and the Weil Positivity Criterion
Results from the Cesàro/Abel-regularization papers and the finitely-supported core of the Weil positivity criterion. Everything in this chapter is fully proved in Lean with no axioms; the honest boundary (the operator theory of the intertwining operator \(\hat W\), and the analytic input that would discharge the positivity hypothesis) is recorded in the module docs and deliberately not claimed.
For \(\sigma \neq 1/2\), the symmetric Cesàro mean \((\int _{1/R}^{R} r^{2\sigma -2}\, dr)/(2\log R)\) tends to \(+\infty \) as \(R \to \infty \). Together with the exact value \(1\) at \(\sigma = 1/2\) (born_rule_cesaro), this makes \(\sigma = 1/2\) the unique locus where the inversion-invariant mean is finite and nonzero.
For \(|\alpha | {\lt} \varepsilon \): \(\tfrac {\varepsilon }{2}\int _{\mathbb R} e^{-\varepsilon |u|}e^{\alpha u}\, du = \varepsilon ^2/(\varepsilon ^2 - \alpha ^2)\).
\(\tfrac {\varepsilon }{2}\int _{\mathbb R} e^{-\varepsilon |u|}\, du = 1\) exactly, for every \(\varepsilon {\gt} 0\).
\(2^{1-s} = 1\) iff \(s = 1 - 2\pi i k/\log 2\) for some \(k \in \mathbb Z\); every such zero has \(\operatorname {Re} s = 1\) (GppCompletedEta.eta_periodic_zero_re), outside the open critical strip.
On the strip \(1 - \varepsilon {\lt} \sigma {\lt} 1 + \varepsilon \): \(\tfrac {\varepsilon }{2}\bigl(\int _0^1 t^{\sigma -2+\varepsilon }\, dt + \int _1^\infty t^{\sigma -2-\varepsilon }\, dt\bigr) = \varepsilon ^2/(\varepsilon ^2-(\sigma -1)^2)\), with value \(1\) at \(\sigma = 1\) and limit \(0\) as \(\varepsilon \to 0^+\) for \(\sigma \neq 1\): the Kronecker-delta selection \(\rho ' = 1-\bar\rho \).
If \(Z \subseteq \mathbb C\) is closed under an involution \(\iota \) and the paired form \(\sum _{\rho \in S} \overline{c(\iota \rho )}\, c(\rho )\) has nonnegative real part on every finite \(S \subseteq Z\), then every point of \(Z\) is fixed by \(\iota \).
The nontrivial zero set of \(\zeta \) is closed under \(\rho \mapsto 1 - \bar\rho \) — a proved theorem (functional equation composed with the proved conjugation symmetry), not an assumption.
Every nontrivial zero lies on the critical line iff the paired form is positive semidefinite on every finite subset of the nontrivial zero set. A rigorous reduction — not a proof of RH: the analytic input that would discharge the positivity hypothesis is not claimed.
\(\int _0^\infty u/\cosh ^2 u\, du = \log 2\) — that is, \(\eta (1) = \log 2\) in Mellin disguise, proved with no series interchange via the explicit antiderivative \(u\tanh u - \log \cosh u\).