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,241 to 1,260 of 1,644 declarations.
lemma
ZetaAbelFractKernel.hasDerivAt_integral_param_dominated_Ioi
Dominated differentiation under ∫_{(1,∞)} F z.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelKernel · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaAbelKernel.lean:162
theorem
ZetaAbelFractKernel.integral_analytic
∫_{(1,∞)} K_z is analytic in z for re z > 0.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelKernel · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaAbelKernel.lean:182
theorem
norm_riemannZeta_ratio_le_on_verticalLine
For σ > 1, the Euler product at re s = 2σ controls ‖ζ(2σ) / ζ σ‖ on the line σ + it.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaConvexity · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaConvexity.lean:38
theorem
norm_riemannZeta_shift_le
If ‖s‖ ≤ 1 and 2 < |t|, then ‖ζ (s + 3/2 + it)‖ < 10 + 2|t|.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaConvexity · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaConvexity.lean:156
theorem
riemannXi_entireOfOrderAtMost_one
The Riemann xi function ξ has order at most one.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaHadamard · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaHadamard.lean:93
theorem
logDeriv_riemannXi_eq_polynomial_derivative_add_tsum
Logarithmic derivative identity for a chosen ξ Hadamard factorization.
The divisor-product differentiability is supplied by
Complex.Hadamard.differentiableAt_divisorCanonicalProduct_univ, and xi zero summability is
supplied by summable_riemannXi_divisorZeroIndex₀_norm_inv_sq. The remaining hypotheses are the
point-not-a-zero assumptions needed for the logarithmic derivative and zero-sum terms; the product
nonvanishing is derived from the generic divisor-product nonvanishing theorem.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaHadamard · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaHadamard.lean:244
theorem
riemannXi_hadamard_polynomial_derivative_eval_eq
Any two xi Hadamard polynomials with the same divisor-canonical product have the same derivative at every point away from the nonzero divisor-indexed zero set.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaHadamard · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaHadamard.lean:294
theorem
existsUnique_riemannXi_hadamard_polynomial_derivative_eval_zero
There is a unique complex number obtained as Polynomial.eval 0 P.derivative from a
degree-one no-monomial Hadamard factorization of Riemann's xi function. This is the canonical
theorem-level formulation of Kadiri's Hadamard constant, without choosing a global witness.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaHadamard · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaHadamard.lean:354
lemma
ZetaPartialSum.tendsto_natCast_cpow_zero_of_neg_re
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaPartialSum · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaPartialSum.lean:167
theorem
ZetaPartialSum.tendsto_riemannZeta
zetaPartialSum converges to riemannZeta for re s > 1.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaPartialSum · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaPartialSum.lean:178
theorem
completedRiemannZeta_two
The completed Riemann zeta factor has value π / 6 at 2.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaValues · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaValues.lean:62
theorem
completedRiemannZeta₀_two
The entire completed zeta function Λ₀ has value (π - 3) / 6 at 2.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaValues · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaValues.lean:84
theorem
completedRiemannZeta₀_nontrivial
The entire completed zeta function Λ₀ is not identically zero.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaValues · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaValues.lean:101
theorem
completedRiemannZeta₀_one_ne_zero
The entire completed zeta function Λ₀ is nonzero at 1.
This uses the Euler-Mascheroni formula for Λ₀(1) from ZetaAsymp, the lower bound
27 / 50 < γ, and an elementary numerical bound log (4π) < 127 / 50.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaValues · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaValues.lean:125
lemma
Complex.exists_completedRiemannZeta₀_right_halfPlane
The functional equation lets one work in the half-plane 1 / 2 ≤ re z.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFiniteOrder · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/ZetaFiniteOrder.lean:75
lemma
Complex.one_sub_re_ge_one_sub_zetaAbelContinuationReLower_of_re_le
If re z ≤ σ₀, then 1 - σ₀ ≤ re (1 - z) for σ₀ = zetaAbelContinuationReLower.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFiniteOrder · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/ZetaFiniteOrder.lean:99
lemma
Complex.norm_mul_riemannZeta_le_exp_of_reflected
Reflected functional-equation factors obey the global zeta growth majorant.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFiniteOrder · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/ZetaFiniteOrder.lean:132
theorem
Complex.completedRiemannZeta_ne_zero_of_one_lt_re
In the half-plane of absolute convergence, the completed zeta function does not vanish.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFiniteOrder · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/ZetaFiniteOrder.lean:454
theorem
Complex.zetaTimesSMinusOne_entire_differentiableOn_compl_singleton
Away from 1, the removable extension is holomorphic as (s - 1)ζ(s).
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFiniteOrder · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/ZetaFiniteOrder.lean:480
theorem
Complex.zetaTimesSMinusOne_entire_continuousAt_one
The residue theorem for ζ gives continuity of the removable extension at 1.
PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFiniteOrder · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/ZetaFiniteOrder.lean:496
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.