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,601 to 1,620 of 1,644 declarations.
lemma
ZetaBnd_aux1p
Big-Oh version of Lemma \ref{ZetaBnd_aux1}.
PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1057
lemma
integrable_log_over_pow
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1099
lemma
integrableOn_of_Zeta0_fun_log
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1135
lemma
hasDerivAt_Zeta0Integral
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1166
lemma
HasDerivAt_cpow_over_var
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1268
lemma
HasDerivAtZeta0
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1284
lemma
Zeta0EqZeta
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1383
lemma
DerivZeta0EqDerivZeta
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1423
lemma
ZetaBnd_aux2
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1457
lemma
UpperBnd_aux2
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1528
lemma
UpperBnd_aux3
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1552
lemma
UpperBnd_aux6
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1598
lemma
ZetaUpperBnd
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1664
lemma
DerivUpperBnd_aux1
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1745
lemma
DerivUpperBnd_aux2
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1779
theorem
DerivUpperBnd_aux3
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1800
theorem
DerivUpperBnd_aux4
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1815
theorem
DerivUpperBnd_aux5
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1829
theorem
DerivUpperBnd_aux6
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1855
lemma
DerivUpperBnd_aux7_1
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1869
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.