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 921 to 940 of 1,644 declarations.
lemma
ArithmeticFunction.LSeries_powR_eq
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:565
lemma
ArithmeticFunction.abscissa_powR_le
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:591
theorem
ArithmeticFunction.LSeries_sigma_eq_riemannZeta_mul
ζ(s)ζ(s - ν) = Σ σ_ν(n) n^(-s) for Re(s) > 1 and Re(s - ν) > 1.
PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:607
lemma
ArithmeticFunction.two_pow_omega_le_sigma_zero
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:724
lemma
ArithmeticFunction.LSeriesSummable.of_norm_le_norm
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:747
lemma
ArithmeticFunction.LSeriesSummable_two_pow_omega
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:766
lemma
ArithmeticFunction.LSeries.term_isMultiplicative_if_fun_isMultiplicative
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:789
lemma
ArithmeticFunction.powOfAdditive_isMultiplicative
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:808
lemma
ArithmeticFunction.two_pow_omega_tsum_prime_pow
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:876
lemma
ArithmeticFunction.Complex.one_add_prime_cpow_ne_zero
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:914
lemma
ArithmeticFunction.two_pow_omega_LSeries_eulerProduct_tprod
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:938
lemma
ArithmeticFunction.two_pow_omega_LSeries_eulerProduct_hasProd
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:963
lemma
ArithmeticFunction.zeta_pow_two
Zeta squared:
ζ(s)^2 = ζ(2*s) * ∑_n (2^omega(n)) n^(-s),
where omega is the number of distinct prime factors.
PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:991
lemma
ArithmeticFunction.LSeriesSummable_moebius_sq
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1030
lemma
ArithmeticFunction.powOfMultiplicative_isMultiplicative
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1054
lemma
ArithmeticFunction.moebius_sq_tsum_prime_pow
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1088
lemma
ArithmeticFunction.moebius_sq_LSeries_eulerProduct_tprod
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1126
lemma
ArithmeticFunction.moebius_sq_LSeries_eulerProduct_hasProd
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1152
lemma
ArithmeticFunction.zeta_alt
Zeta alt:
ζ(s) = ζ(2*s) * ∑_n (|μ(n)|) n^(-s),
where omega is the number of distinct prime factors.
PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1183
lemma
ArithmeticFunction.pow_divisors_mul
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1213
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.