The functional equation for the logarithmic derivative of the Riemann zeta function

Differentiating the functional equation riemannZeta_one_sub logarithmically gives an identity relating ζ'/ζ (s) and ζ'/ζ (1 - s), involving the digamma function ψ and a tangent term.

Main statements

• logDeriv_riemannZeta_one_sub: for s not an integer with ζ s ≠ 0, ζ'/ζ (s) = -ζ'/ζ (1 - s) + log (2 π) - ψ s + (π / 2) * tan (π s / 2).

theorem logDeriv_riemannZeta_one_sub {s : ℂ} (hs : ∀ (n : ℤ), s ≠ ↑n) (hz : riemannZeta s ≠ 0) : logDeriv riemannZeta s = -logDeriv riemannZeta (1 - s) + Complex.log (2 * ↑Real.pi) - s.digamma + ↑Real.pi / 2 * Complex.tan (↑Real.pi * s / 2)

The functional equation for the Riemann zeta function, in logarithmic-derivative form. For s not an integer with riemannZeta s ≠ 0, ζ'/ζ (s) = -ζ'/ζ (1 - s) + log (2 π) - ψ s + (π / 2) * tan (π s / 2), where ψ is the digamma function.