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,281 to 1,300 of 1,644 declarations.
theorem
SelbergSieve.selberg_bound_muPlus
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Selberg.lean:395
lemma
Sieve.prodDistinctPrimes_squarefree
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean:30
theorem
Sieve.prime_dvd_primorial_iff
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean:63
theorem
Sieve.siftedSum_eq
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean:79
theorem
Sieve.prod_factors_one_div_compMult_ge
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean:157
theorem
Sieve.prod_factors_sum_pow_compMult
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean:190
theorem
Sieve.selbergBoundingSum_ge_sum_div
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean:364
theorem
Sieve.boundingSum_ge_sum
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean:464
theorem
Sieve.boundingSum_ge_log
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean:496
theorem
Sieve.rem_sum_le_of_const
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean:511
lemma
Metric.eannulusIoc_ofReal
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Annulus · PrimeNumberTheoremAnd/Mathlib/Topology/MetricSpace/Annulus.lean:375
lemma
Metric.eannulusIcc_ofReal
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Annulus · PrimeNumberTheoremAnd/Mathlib/Topology/MetricSpace/Annulus.lean:409
theorem
cauchySeq_of_dist_le_of_one_le
If dist (s n) (s m) ≤ b m for all 1 ≤ m ≤ n and b tends to zero, then s is Cauchy.
PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Cauchy · PrimeNumberTheoremAnd/Mathlib/Topology/MetricSpace/Cauchy.lean:19
theorem
LogDerivativeDirichlet
It has already been established that zeta doesn't vanish on the 1 line, and has a pole at of order 1. We also have the following.
PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:58
lemma
smoothedChebyshevIntegrand_conj
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:102
theorem
SmoothedChebyshevDirichlet
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:262
theorem
SmoothedChebyshevClose
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:689
theorem
SmoothedChebyshevPull1
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:1122
lemma
verticalIntegral_split_three_finite
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:1314
lemma
verticalIntegral_split_three_finite'
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.MediumPNT · PrimeNumberTheoremAnd/MediumPNT.lean:1330
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.