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 1,361 to 1,380 of 1,644 declarations.
lemma
Perron.tendsto_zero_Lower
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:679
lemma
Perron.tendsto_zero_Upper
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:700
lemma
Perron.contourPull
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:717
lemma
Perron.formulaLtOne
We are ready for the first case of the Perron formula, namely when :
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:731
theorem
Perron.HolomorphicOn.upperUIntegral_eq_zero
The second case is when . Here are some auxiliary lemmata for the second case. TODO: Move to more general section
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:780
theorem
Perron.HolomorphicOn.lowerUIntegral_eq_zero
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:793
lemma
Perron.bddAbove_square_of_tendsto
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:840
lemma
Perron.diffBddAtZero
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:849
lemma
Perron.diffBddAtNegOne
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:894
lemma
Perron.residueAtZero
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:938
lemma
Perron.residueAtNegOne
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:980
lemma
Perron.residuePull1
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:1020
lemma
Perron.residuePull2
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:1059
lemma
Perron.formulaGtOne
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:1119
lemma
rect_subset_iff
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Rectangle · PrimeNumberTheoremAnd/Rectangle.lean:103
lemma
rectangle_disjoint_singleton
Note: try using by simp for h.
PrimeNumberTheoremAnd.Rectangle · PrimeNumberTheoremAnd/Rectangle.lean:144
theorem
Complex.nhds_hasBasis_square
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Rectangle · PrimeNumberTheoremAnd/Rectangle.lean:253
lemma
logDeriv_sub_principal_isBigO_one_of_meromorphicOrderAt
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.RectangleArgumentPrinciple · PrimeNumberTheoremAnd/RectangleArgumentPrinciple.lean:58
theorem
logDeriv_hasSimplePolesOn_of_meromorphicOrderAt_ne_top
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.RectangleArgumentPrinciple · PrimeNumberTheoremAnd/RectangleArgumentPrinciple.lean:194
theorem
logDeriv_poles_eq_divisor_support
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.RectangleArgumentPrinciple · PrimeNumberTheoremAnd/RectangleArgumentPrinciple.lean:212
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.