AlexKontorovich/PrimeNumberTheoremAnd

PrimeNumberTheoremAnd

Blueprint for the PNT+ Project

Therefore indexed 1,644 complete source declarations from the exact package revision. Individual authorship and independent verification remain unset.

Research project325 GitHub starsApache-2.09 indexed versionsRepository Full history on Reservoir

Head version

a93551347dce

a93551347dce924b1db75d40218841bf085a465f

Toolchain: leanprover/lean4:v4.32.0
Revision date: 22 Jul 2026
Dependencies: 13
Versions: 9

External build observation

Exact head commit and toolchain

No Reservoir build observation was found for this exact commit and toolchain. This is not evidence of failure.

Pin this source in lakefile.lean

require PrimeNumberTheoremAnd from git "https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git" @ "a93551347dce924b1db75d40218841bf085a465f"

Source declarations

1,644 indexed proofs

Package history

Showing 1,621 to 1,640 of 1,644 declarations.

lemma

DerivUpperBnd_aux7_3

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1883

lemma

DerivUpperBnd_aux7_tendsto

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1911

theorem

DerivUpperBnd_aux7

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1959

lemma

ZetaDerivUpperBnd

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:2129

lemma

Tendsto_nhdsWithin_punctured_map_add

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:2176

lemma

riemannZeta_isBigO_near_one_horizontal

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:2206

lemma

ZetaNear1BndExact

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:2241

lemma

norm_zeta_product_ge_one

For positive x and nonzero y we have that $|\zeta(x)^3 \cdot \zeta(x+iy)^4 \cdot \zeta(x+2iy)| \ge 1$ .

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:2302

lemma

ZetaLowerBound3

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:2359

lemma

ZetaInvBound1

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:2456

lemma

ZetaInvBound2

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:2507

lemma

Zeta_eq_int_derivZeta

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:2614

lemma

Zeta_diff_Bnd

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:2650

lemma

ZetaInvBnd_aux2

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:2686

lemma

ZetaInvBnd

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:2705

lemma

Annoyingly, it is not immediate from this that $\zeta$ doesn't vanish there! That's because $1/0 = 0$ in Lean. So we give a second proof of the same fact (refactor this later), with a lower bound on $\zeta$ instead of upper bound on $1 / \zeta$ .

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:2822

lemma

ZetaZeroFree

Now we get a zero free region.

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:2963

lemma

LogDerivZetaBnd

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:3000

lemma

ZetaNoZerosInBox

Then, since $\zeta$ doesn't vanish on the 1-line, there is a $\sigma<1$ (depending on $T$ ), so that the box $[\sigma,1] \times_{ℂ} [-T,T]$ is free of zeros of $\zeta$ .

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:3096

theorem

LogDerivZetaHolcSmallT

We now prove that there's an absolute constant $\sigma_0$ so that $\zeta'/\zeta$ is holomorphic on a rectangle $[\sigma_2,2] \times_{ℂ} [-3,3] \setminus \{1\}$ .

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:3237

Static source extraction only. Package code was not executed. Every result keeps its complete declaration, exact file and line range, commit, toolchain, license file, and content hash.