MediumPNT

TheoremGenStrengthPNT#

Assuming a bound of the form of Definition LogDerivZetaHasBound, we have that

\[ \sum_{n \leq x}\Lambda(n)=x+O(x\exp(-c(\log x)^{1/(1+n_1)})). \]

Proof

By Theorems SmoothedChebyshevPull1, SmoothedChebyshevPull2, and SmoothedChebyshevClose we have that

\[ \mathcal{M}(\tilde{1}_\varepsilon)(1)\,x^1+I_1-I_2+I_3-I_4+I_5+I_6+I_7+I_8+I_9 =\psi(x)+O(\varepsilon x\log x). \]

Applying Theorems I1Bound, I2GenBound, I3GenBound, I4GenBound, I5Bound, I6GenBound, I7GenBound, I8GenBound, I9Bound, and MellinOfSmooth1c we have

\[ \psi(x)=x+O(\varepsilon x)+O(\varepsilon x\log x)+O\left(\frac{X}{\varepsilon T}\right)+ O\left(\frac{X\log X}{\varepsilon T}\right)+ O\left(\frac{X}{\varepsilon}\,X^{-A/(\log T)^{n_1}}\right)+ O\left(\frac{X^{\sigma_2}}{\varepsilon}\right). \]

Balancing the error terms in \(\varepsilon\) and \(T\) completes the proof.

Lean

Formalized as GenStrengthPNT.

Sources

• PNT+ blueprint: PrimeNumberTheoremAnd/MediumPNT.lean

LeanGenStrengthPNT

Uses 32 · Used by 2

Statement usesLogDerivZetaHasBound

Proof usesI7GenBound · I3GenBound · LogDerivZetaHolcSmallT · I₄ · I₂ · I₆ · I5Bound · I4GenBound · SmoothedChebyshevClose · I₃ · I₁ · Smooth1Nonneg · MellinOfSmooth1c · Smooth1ContinuousAt · I6GenBound · I1Bound · I₃₇ · I₉ · Smooth1Properties-above · Smooth1 · I₈ · I₅ · I8GenBound · SmoothedChebyshev · SmoothedChebyshevPull2 · SmoothExistence · I9Bound · I2GenBound · I₇ · Smooth1LeOne · SmoothedChebyshevPull1

Used byMediumPNT · StrongPNT

TheoremMediumPNT#

We have

\[ \sum_{n \leq x}\Lambda(n)=x+O(x \exp(-c(\log x)^{1/10})). \]

Proof

This follows as a corollary of Theorems GenStrengthPNT and LogDerivZetaBnd.

Lean

Formalized as MediumPNT.

Sources

• PNT+ blueprint: PrimeNumberTheoremAnd/MediumPNT.lean

LeanMediumPNT

Uses 4

Proof usesLogDerivZetaHolcLargeT9 · LogDerivZetaBndUnif99 · LogDerivZetaHasBound · GenStrengthPNT

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.