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 201 to 220 of 1,644 declarations.

theorem

CH2.prop_2_3_1

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

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:82

theorem

CH2.prop_2_3

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

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:622

theorem

CH2.S_eq_I

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

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:682

theorem

CH2.prop_2_4_plus

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

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:892

theorem

CH2.prop_2_4_minus

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

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1061

theorem

CH2.tanh_add_int_mul_pi_I

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

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1145

lemma

CH2.meromorphicOrderAt_cosh_ne_top

Complex.cosh is not identically zero near any point, so its meromorphicOrderAt is finite.

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1260

lemma

CH2.meromorphicOrderAt_sinh_ne_top

Complex.sinh is not identically zero near any point, so its meromorphicOrderAt is finite.

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1276

lemma

CH2.meromorphicOrderAt_coth_lt_zero_iff

coth has a pole at z if and only if sinh z = 0.

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1292

theorem

CH2.Phi_circ.poles

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

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1345

theorem

CH2.Phi_circ.residue

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

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1408

theorem

CH2.Phi_circ.poles_simple

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

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1473

theorem

CH2.B.continuous_zero

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

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1515

theorem

CH2.B.continuousAt_ofReal_ne_zero

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

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1554

lemma

CH2.meromorphicAt_B

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

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1595

theorem

CH2.analyticAt_B

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

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1617

theorem

CH2.Phi_star.meromorphic

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

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1686

theorem

CH2.Phi_star.poles

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

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1702

theorem

CH2.Phi_star.residue

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

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1836

theorem

CH2.Phi_star.poles_simple

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

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1890

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.