Strong PNT
1
Complex Analysis
▶
1.1
Borel-Carathéodory I
1.2
Borel-Carathéodory II
1.3
Integral Antiderivative
1.4
Complex logarithm
2
Log Derivative
▶
2.1
\(B_f\) analytic and never zero
2.2
Bounding \(K\le 3\log B\)
2.3
Log \(L_f\)
2.4
Log derivative \(L_f'\) expansion
3
Riemann Zeta Function
▶
3.1
Zeta lower bound
3.2
Zeta bound
3.3
Zeta derivatives
4
Zero Free Region
▶
4.1
Bound on \(\zeta '/\zeta \)
5
Strong PNT
Dependency graph
5 Strong PNT
Theorem
621
Strong PNT
✓
#
L∃∀N
Lean declarations
Strong_PNT
We have
\[ \sum _{n \leq x} \Lambda (n) = x + O(x \exp (-c(\log x)^{1/2})). \]
Proof
▶