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,301 to 1,320 of 1,644 declarations.

theorem

SmoothedChebyshevPull2_aux1

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

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:1347

theorem

SmoothedChebyshevPull2

Next pull contours to another box.

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:1370

theorem

ZetaBoxEval

We insert this information in $\psi_{\epsilon}$ . We add and subtract the integral over the box $[1-\delta,2] \times_{ℂ} [-T,T]$ , which we evaluate as follows

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:1569

theorem

poisson_kernel_integrable

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

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:1601

theorem

ae_volume_of_contains_compl_singleton_zero

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

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:1616

theorem

integral_evaluation

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

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:1645

lemma

IBound_aux1

This auxiliary lemma is useful for what follows.

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:1724

lemma

I9I1

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

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:2136

theorem

I9Bound

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

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:2150

lemma

I2Bound

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

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:2171

lemma

I8I2

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

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:2353

lemma

I8Bound

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

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:2379

lemma

log_pow_over_xsq_integral_bounded

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

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:2410

lemma

I7I3

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

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:2976

lemma

I7Bound

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

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:2990

lemma

I6Bound

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

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:3410

lemma

I5Bound

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

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:3427

lemma

LogDerivZetaBoundedAndHolo

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

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:3591

lemma

MellinOfSmooth1cExplicit

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

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:3617

lemma

x_ε_to_inf

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

PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:3637

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.