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,421 to 1,440 of 1,644 declarations.
lemma
BlaschkeNonzero
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:714
theorem
ZerosBound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:808
theorem
JBlaschkeDerivBound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:881
lemma
ZetaFixedLowerBound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:1121
lemma
Zeta1AltFormula
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:1187
theorem
GlobalBound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:1254
lemma
LogDerivZetaBdd_of_Re_ge_three_halves
The logarithmic derivative of the Riemann zeta function is bounded in the half-plane
Re(s) >= 3/2.
PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:1747
theorem
LogDerivZetaUniformLogSquaredBound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:1807
lemma
IntegralLogSqOverTSqBound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:1928
lemma
LogDerivZetaBoundForI1
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:1986
lemma
I1NewIntegrandBound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:2004
lemma
I1NewBound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:2047
lemma
I5NewBound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:2172
lemma
I4NewBound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:2275
theorem
SmoothedChebyshevPull3
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:2365
theorem
hardy_sigma_delayed_eq
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:68
theorem
hardy_sigma_delayed_tendsto
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:83
theorem
hardy_sigma_delayed_sub_s_eq
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:128
theorem
hardy_sigma_delayed_bound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:152
lemma
k_n_properties
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:177
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.