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 841 to 860 of 1,644 declarations.

theorem

Rosser1941.p_n_lower

Some results from \cite{rosser1941}

PrimeNumberTheoremAnd.IEANTN.TMEEMT · PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1047

theorem

RamareSaouter2003.has_prime_in_interval_2

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

PrimeNumberTheoremAnd.IEANTN.TMEEMT · PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1475

theorem

ZetaAppendix.integral_power_phase_ibp

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

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:226

theorem

\subsection{The decay of a Fourier transform} Our first objective will be to estimate the Fourier transform of $t^{-s} \mathbb{1}_{[a,b]}$ . In particular, we will show that, if $a$ and $b$ are half-integers, the Fourier cosine transform has quadratic decay {\em when evaluated at integers}. In general, for real arguments, the Fourier transform of a discontinuous function such as $t^{-s} \mathbb{1}_{[a,b]}$ does not have quadratic decay.

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:378

theorem

ZetaAppendix.lemma_aachra

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

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:457

theorem

ZetaAppendix.lemma_IBP_bound_C1

For C¹ functions g and F, the error in integration by parts is bounded by sup ‖F‖ · ∫ |g'|.

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:578

theorem

ZetaAppendix.lemma_IBP_bound_C1_monotone

Integration by parts bound for C¹ monotone functions. For C¹ monotone g and C¹ F, ‖∫ g F' - [gF]‖ ≤ sup ‖F‖ · (g(b) - g(a)).

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:703

theorem

ZetaAppendix.bernsteinApproximation_monotone

The Bernstein approximation of a monotone function is monotone.

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:743

theorem

ZetaAppendix.lemma_approx_monotone_C1_I

Continuous monotone functions on [0,1] can be uniformly approximated by smooth monotone functions (polynomials).

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:831

theorem

ZetaAppendix.lemma_approx_monotone_C1

Continuous monotone functions on a compact interval can be uniformly approximated by C¹ monotone functions.

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:849

theorem

ZetaAppendix.lemma_IBP_bound_monotone

Integration by parts bound for continuous monotone functions. For continuous monotone g and C¹ F, ‖∫ g F' - [gF]‖ ≤ sup ‖F‖ · (g(b) - g(a)).

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:883

theorem

ZetaAppendix.lemma_IBP_bound_abs_antitone

Integration by parts bound for continuous functions with antitone absolute value. If |g| is antitone, ‖∫ g F'‖ ≤ sup ‖F‖ · 2 |g(a)|.

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:950

theorem

ZetaAppendix.lemma_aachmonophase

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

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:1028

theorem

ZetaAppendix.lemma_aachdecre

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

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:1091

lemma

ZetaAppendix.lemma_aachcanc_pointwise

At half-integers, (Φ n t + Φ (-n) t) / 2 = Ψ t where Φ and Ψ are as in lemma_aachcanc.

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:1553

theorem

ZetaAppendix.lemma_aachcanc

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

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:1604

theorem

ZetaAppendix.lemma_abadeulmac'

\subsection{Approximating zeta(s)} We start with an application of Euler-Maclaurin.

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:1752

theorem

ZetaAppendix.lemma_abadeulmac

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

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:1822

theorem

ZetaAppendix.lemma_abadtoabsum

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

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:1936

lemma

ZetaAppendix.lemma_abadsumas_integrable_explog

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

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2005

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.