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,221 to 1,240 of 1,644 declarations.
lemma
Nat.Primes.norm_cpow_neg_lt_one
For a prime p and s with real part > 1, ‖p^{-s}‖ < 1.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:58
lemma
Nat.Primes.norm_one_sub_cpow_neg_vertical_le
On the vertical line σ + it, ‖1 - p^{-s}‖ ≤ 1 + p^{-σ}.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:99
lemma
Nat.Primes.one_sub_cpow_neg_vertical_ne_zero
On the vertical line σ + it with 1 < σ, the Euler factor 1 - p^{-s} is nonzero.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:110
lemma
Nat.Primes.multipliable_inv_one_add
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:130
lemma
Nat.Primes.multipliable_complex_inv_one_add
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:140
lemma
Nat.Primes.inv_one_sub_sq_eq_mul_inv_one_sub_one_add
(1 - z²)⁻¹ = (1 - z)⁻¹ · (1 + z)⁻¹ for ‖z‖ < 1.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:152
lemma
Nat.Primes.eulerFactor_two_mul
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:167
theorem
riemannZeta_eq_mul_tprod_inv_one_add
ζ(2r) = ζ(r) · ∏_p (1 + p^{-r})⁻¹ for real r > 1.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:188
theorem
riemannZeta_div_riemannZeta_eq_tprod_inv_one_add
ζ(2r)/ζ(r) = ∏_p (1 + p^{-r})⁻¹ for real r > 1.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:211
theorem
norm_riemannZeta_eulerProduct
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:224
theorem
norm_riemannZeta_div_riemannZeta
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:234
theorem
tprod_inv_one_add_real_le_riemannZeta_norm_on_verticalLine
On the vertical line re s = σ > 1, the real product ∏_p (1 + p^{-σ})^{-1} is dominated
by the Euler product at σ + it.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:284
theorem
riemannZeta_abel_integral
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelContinuation · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaAbelContinuation.lean:106
theorem
norm_zetaAbelContinuationFormula_le
On zetaAbelContinuationDomain, the Abel formula satisfies the standard strip bound.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelContinuation · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaAbelContinuation.lean:145
theorem
riemannZeta_eq_zetaAbelContinuationFormula
The Abel integral formula agrees with ζ on zetaAbelContinuationDomain.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelContinuation · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaAbelContinuation.lean:196
theorem
norm_zetaAbelFractKernel_le
{u} · u^{-s-1} is dominated by u^{- re s - 1} for u ≥ 1.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelKernel · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaAbelKernel.lean:44
lemma
ZetaAbelFractKernel.intervalIntegrable
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelKernel · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaAbelKernel.lean:73
theorem
ZetaAbelFractKernel.integrableOn_Ioi
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelKernel · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaAbelKernel.lean:102
theorem
ZetaAbelFractKernel.hasDerivAt_in_param
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelKernel · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaAbelKernel.lean:129
theorem
ZetaAbelFractKernel.kernel_deriv_norm_bound_on_ball
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelKernel · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaAbelKernel.lean:140
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.