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 901 to 920 of 1,644 declarations.

lemma

ZetaAppendix.lemma_abadimpseri

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

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

lemma

ZetaAppendix.lemma_abadsumas_summable_alternating_theta

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

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

lemma

ZetaAppendix.proposition_dadaro_b_tendsto_zero_atTop

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

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

lemma

riemannZeta.zeroes_on_Compact_finite

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

PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions · PrimeNumberTheoremAnd/IEANTN/ZetaDefinitions.lean:61

lemma

riemannZeta.zeroes_on_Compact_finite'

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

PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions · PrimeNumberTheoremAnd/IEANTN/ZetaDefinitions.lean:90

lemma

eSHP.exists_prime_gap_record_le

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

PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP · PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:133

lemma

eSHP.nth_prime_vals

Values of the first 9 primes (0-indexed).

PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP · PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:308

lemma

eSHP.first_gap_odd_gt_1

For any odd number g > 1, the first prime gap of size g is 0 (meaning it doesn't exist).

PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP · PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:341

lemma

eSHP.first_gap_4

The first prime gap of size 4 occurs at prime 7.

PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP · PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:379

lemma

eSHP.first_gap_6

The first prime gap of size 6 occurs at prime 23.

PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP · PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:394

theorem

eSHP.exists_prime_gap

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

PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP · PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:453

theorem

ArithmeticFunction.sum_moebius_pmul_eq_prod_one_sub

If g is a multiplicative arithmetic function, then for any $n \neq 0$ , $\sum_{d | n} \mu(d) \cdot g(d) = \prod_{p | n} (1 - g(p))$ .

PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:99

theorem

ArithmeticFunction.zeta_mul_zeta

The Dirichlet convolution of $\zeta$ with itself is $\tau$ (the divisor count function).

PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:148

theorem

ArithmeticFunction.LSeries_tau_eq_riemannZeta_sq

The L-series of $\tau$ equals the square of the Riemann zeta function for $\Re(s) > 1$ .

PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:169

theorem

ArithmeticFunction.LSeries_d_summable

The L-series for d k is summable

PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:239

theorem

ArithmeticFunction.LSeries_d_eq_riemannZeta_pow

The L-series of d k equals ζ(s)^k for Re(s) > 1.

PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:258

theorem

ArithmeticFunction.d_apply_prime_pow

Explicit formula: d k (p^a) = (a + k - 1).choose (k - 1) for prime p for k ≥ 1.

PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:303

lemma

ArithmeticFunction.d_apply

(1.25) in Iwaniec-Kowalski: a formula for d_k for all n.

PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:321

theorem

ArithmeticFunction.isMultiplicative_powR

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

PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:495

lemma

ArithmeticFunction.sigmaR_eq_zeta_mul_powR

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

PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:516

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.