Skip to main content
therefore
Sign inSign up
Open navigation
All packages

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 versionsRepositoryFull 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 881 to 900 of 1,644 declarations.

lemma

ZetaAppendix.second_ibp_expr_add_adjacent

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

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

lemma

ZetaAppendix.neg_B1_integral_add_adjacent

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

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

lemma

ZetaAppendix.integral_cpow_neg_eq_main

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

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

theorem

ZetaAppendix.lemma_abadusepoisson

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

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

lemma

ZetaAppendix.hsummable''

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

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

theorem

ZetaAppendix.tsum_even_add_odd'

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

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

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.