Head version
a93551347dce
a93551347dce924b1db75d40218841bf085a465f
- Toolchain
- leanprover/lean4:v4.32.0
- Revision date
- 22 Jul 2026
- Dependencies
- 13
- Versions
- 9
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.
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
Showing 161 to 180 of 1,644 declarations.
theorem
Buthe.table_1_to_32e12
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Buthe · PrimeNumberTheoremAnd/IEANTN/Buthe.lean:146
lemma
CH2.LadderParams.upperRectangle_subset_Rpos
The rectangle used in lemma_5_1_a is contained in Rpos.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:341
lemma
CH2.upperRectangle_meromorphicOn
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:762
lemma
CH2.upperRectangleIntegral'_eq_sumResiduesIn
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:802
lemma
CH2.intVSeg_eq_intCnPlus_add_rectangleIntegral
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:825
lemma
CH2.sumResiduesIn_upperRectangle_eq_sumResiduesIn_Rpos
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:874
lemma
CH2.upperRectangle_no_poles_boundary
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:917
theorem
CH2.lemma_5_1_a
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1224
lemma
CH2.intVSeg_eq_intCnMinus_add_rectangleIntegral
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1333
lemma
CH2.LadderParams.lowerRectangle_subset_RposBar
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1374
lemma
CH2.lowerRectangle_meromorphicOn
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1386
lemma
CH2.meromorphicOrderAt_starRingEnd
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1504
lemma
CH2.lowerRectangle_no_poles_boundary
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1540
lemma
CH2.sumResiduesIn_lowerRectangle_eq_sumResiduesIn_RposBar
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1662
theorem
CH2.lemma_5_1_b
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1739
lemma
CH2.intCn1Plus_add_intCn1Minus_eq_rectangleIntegral_add_verticalAt
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1805
lemma
CH2.centralRectangle_subset_RC
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1847
lemma
CH2.centralRectangle_no_poles_boundary
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1982
lemma
CH2.centralRectangleIntegral'_eq_sumResiduesIn
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:1998
lemma
CH2.sumResiduesIn_centralRectangle_eq_sumResiduesIn_RC
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2036
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.