LogDerivZetaBndUnif99

LemmaLogDerivZetaBndUnif99#

There exist \(A, C > 0\) such that

\[ |\frac{\zeta'}{\zeta}(\sigma + it)|\leq C \log |t|^9 \]

whenever \(|t|>3\) and \(\sigma > 1 - A/\log |t|^9\).

Proof

For \(\sigma\) close to \(1\) use Lemma LogDerivZetaBnd, otherwise estimate trivially.

Lean

Formalized as LogDerivZetaBndUnif99.

Sources
LeanLogDerivZetaBndUnif99
Uses 2 · Used by 1
Proof usesriemannZetaLogDerivResidue · LogDerivZetaBnd
Used byMediumPNT

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.