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 581 to 600 of 1,644 declarations.
theorem
meromorphicOrderAt_le_deriv_add_one
The order of the derivative is at least the order minus one.
PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:47
theorem
meromorphicAt_riemannZeta
The Riemann zeta function is meromorphic at every point.
PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:65
theorem
meromorphicOrderAt_riemannZeta_ne_top
The Riemann zeta function is not locally zero anywhere.
PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:90
theorem
meromorphicOrderAt_riemannZeta_one
The Riemann zeta function has a simple pole at s = 1: its meromorphic order there is -1.
PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:106
theorem
neg_one_le_meromorphicOrderAt_neg_zeta_logDeriv
The negative logarithmic derivative -ζ'/ζ has at most a simple pole at every point.
PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:121
theorem
abs_mul_exp_isBigO
Keystone: a linear weight is absorbed by an exponential with a slightly smaller rate.
PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:148
theorem
neg_id_mul_decay
The decay hypothesis transfers from φ to -(·)·φ with a slightly smaller rate.
PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:164
theorem
laplace_integrand_integrable
The Laplace integrand φ(y)·e^{-σy} is integrable for σ in the convergence strip.
PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:176
theorem
laplace_deriv_integrand_integrable
The derivative integrand -(y)·φ(y)·e^{-σy} is integrable for σ in the strip.
PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:230
theorem
Phi_differentiableAt
The bilateral Laplace transform Φ(s) = ∫ φ(y) e^{-sy} dy is differentiable on the strip.
PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:245
theorem
Phi_analyticOnNhd
The bilateral Laplace transform is analytic on the strip -(1+b) < Re s < b.
PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:316
theorem
tendsto_sub_mul_neg_zeta_logDeriv
The limit (z-p)·(-ζ'/ζ)(z) → -order(ζ,p) (residue of the log-derivative = order).
PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:329
theorem
rectangleIntegral'_eq12
Side identification: the rectangle integral of f over the box [-a,1+a]×[-T,T]
splits into the two vertical and two horizontal pieces appearing in eq. (12).
PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:358
theorem
residue_neg_zeta_logDeriv_mul
Residue value (Part 4, with the analytic cofactor Φ(-·)): the residue of
s ↦ (-ζ'/ζ)(s)·Φ(-s) at p equals -order(ζ, p)·Φ(-p).
PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:380
theorem
meromorphicOn_eq12_integrand
The eq.(12) integrand f(s) = (-ζ'/ζ)(s)·Φ(-s) is meromorphic on the rectangle
[-a,1+a]×[-T,T].
PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:412
theorem
hasSimplePolesOn_eq12_integrand
The eq.(12) integrand has at most simple poles on the rectangle: its meromorphic order is
≥ -1 at every point (the -ζ'/ζ factor contributes ≥ -1, the analytic Φ(-·) factor ≥ 0).
PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:425
theorem
eq12_meromorphicOrderAt_nonneg_of_ne
At a point of the box where ζ ≠ 0 and s ≠ 1, the eq.(12) integrand is analytic, so its
meromorphic order is non-negative (no pole).
PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:447
theorem
eq12_no_border_poles
No poles on the rectangle border (residue-theorem hyp B2/B3): given that ζ is non-zero and
the point is ≠ 1 on the entire border, the eq.(12) integrand is analytic there, hence has
non-negative order, so the border is disjoint from the pole set.
PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:464
theorem
sumResiduesIn_eq12_eq
Part 5 (residue bookkeeping): the sum of residues of the eq.(12) integrand f over the poles
inside the rectangle equals Φ(-1) - zeroes_sum. The two pole contributions are s = 1
(residue Φ(-1)) and the non-trivial zeros ρ (residue -ord(ρ)·Φ(-ρ)); the set-characterization
of the pole set and the residue values are supplied at the call site.
PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:492
lemma
Kadiri.kadiri_laplace_positive_line_weight_integrable_of_continuous
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.KadiriEq13 · PrimeNumberTheoremAnd/IEANTN/KadiriEq13.lean:38
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.