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,261 to 1,280 of 1,644 declarations.
theorem
Complex.zetaTimesSMinusOne_entire_differentiable
The removable extension of (s - 1)ζ(s) is entire.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFiniteOrder · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/ZetaFiniteOrder.lean:512
theorem
Aux.conv_lambda_sq_larger_sum
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean:42
theorem
Aux.moebius_inv_dvd_lower_bound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean:61
theorem
Aux.sum_inv_le_log
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean:156
theorem
Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean:185
theorem
Aux.sum_pow_cardDistinctFactors_le_self_mul_log_pow
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean:253
theorem
SelbergSieve.one_div_selbergTerms_eq_conv_moebius_nu
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Basic.lean:98
theorem
SelbergSieve.nu_eq_conv_one_div_selbergTerms
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Basic.lean:115
theorem
SelbergSieve.conv_selbergTerms_eq_selbergTerms_mul_nu
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Basic.lean:129
theorem
SelbergSieve.lambdaSquared_eq_zero_of_support
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Basic.lean:176
theorem
SelbergSieve.upperMoebius_of_lambda_sq
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Basic.lean:202
theorem
SelbergSieve.lambdaSquared_mainSum_eq_quad_form
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Basic.lean:233
theorem
SelbergSieve.lambdaSquared_mainSum_eq_diag_quad_form
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Basic.lean:260
theorem
SelbergSieve.selbergWeights_mul_mu_nonneg
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Selberg.lean:96
lemma
SelbergSieve.sum_mul_subst
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Selberg.lean:116
theorem
SelbergSieve.selbergWeights_eq_dvds_sum
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Selberg.lean:157
theorem
SelbergSieve.selbergWeights_diagonalisation
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Selberg.lean:199
theorem
SelbergSieve.selberg_bound_simple_mainSum
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Selberg.lean:263
theorem
SelbergSieve.selbergBoundingSum_ge
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Selberg.lean:310
theorem
SelbergSieve.selberg_bound_weights
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Selberg.lean:380
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.