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,401 to 1,420 of 1,644 declarations.

lemma

sumResiduesIn_inter_eq_of_set_eq

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

PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:1243

theorem

sin_div_error_pointwise_bound

Pointwise bound on the sin-div windowed error term: scaling by the normalized sinc kernel and a mean-value estimate on g (x - u) - g x gives a bound D / π that is independent of the height T.

PrimeNumberTheoremAnd.SincKernelErrorBounds · PrimeNumberTheoremAnd/SincKernelErrorBounds.lean:21

theorem

sin_div_error_interval_bound

Interval form of sin_div_error_pointwise_bound: integrating the pointwise bound over [-1, 1] controls the windowed error integral by (D / π) · vol (Ioc (-1) 1).

PrimeNumberTheoremAnd.SincKernelErrorBounds · PrimeNumberTheoremAnd/SincKernelErrorBounds.lean:60

lemma

smooth_urysohn_support_Ioo

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

PrimeNumberTheoremAnd.SmoothExistence · PrimeNumberTheoremAnd/SmoothExistence.lean:12

lemma

SmoothExistence

Let $\nu$ be a bumpfunction.

PrimeNumberTheoremAnd.SmoothExistence · PrimeNumberTheoremAnd/SmoothExistence.lean:50

lemma

W1.iteratedDeriv_sub

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

PrimeNumberTheoremAnd.Sobolev · PrimeNumberTheoremAnd/Sobolev.lean:144

theorem

W21_approximation

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

PrimeNumberTheoremAnd.Sobolev · PrimeNumberTheoremAnd/Sobolev.lean:227

lemma

AnalyticOn.norm_le_of_norm_le_on_sphere

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

PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:30

theorem

borelCaratheodory'

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

PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:59

lemma

cauchy_formula_deriv

This upstreamed from https://github.com/math-inc/strongpnt/tree/main

PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:100

lemma

DerivativeBound

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

PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:124

theorem

BorelCaratheodoryDeriv

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

PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:179

theorem

\begin{definition}[TaxicabIntegral]\label{TaxicabIntegral} Let $0 < R$ . Let $f:\overline{\mathbb{D}_R}\to\mathbb{C}$ be analytic on neighborhoods of points in $\overline{\mathbb{D}_R}$ . Define the functon $I_f:\mathbb{D}_R\to\mathbb{C}$ by $I_f(z)=z\int_0^1f(tz)\,dt.$ \end{definition}

PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:221

lemma

ZeroFactorization

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

PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:382

lemma

analyticAt_finset_prod_sub_pow

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

PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:456

lemma

CfAnalytic

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

PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:470

lemma

BlaschkeAnalytic

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

PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:547

lemma

BlaschkeOfZero

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

PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:577

lemma

norm_fOfZero_le_norm_BlaschkeOfZero

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

PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:614

lemma

DiskBound

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

PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:653

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.