Skip to main content
therefore
Sign inSign up
Open navigation
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.

Research project325 GitHub starsApache-2.09 indexed versionsRepositoryFull history on Reservoir

Head version

a93551347dce

a93551347dce924b1db75d40218841bf085a465f

Toolchain
leanprover/lean4:v4.32.0
Revision date
22 Jul 2026
Dependencies
13
Versions
9

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

Package history

Showing 541 to 560 of 1,644 declarations.

theorem

Kadiri.hadamardGenusOneFactor_pair_cancellation

Pairing the genus-one factors at opposite zeros cancels the exponential corrections.

PrimeNumberTheoremAnd.IEANTN.HadamardLogDerivative · PrimeNumberTheoremAnd/IEANTN/HadamardLogDerivative.lean:24

theorem

Kadiri.logDeriv_centeredHadamardOrbitBlock

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.HadamardLogDerivative · PrimeNumberTheoremAnd/IEANTN/HadamardLogDerivative.lean:81

theorem

Kadiri.logDeriv_completedZetaFactor

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.HadamardLogDerivative · PrimeNumberTheoremAnd/IEANTN/HadamardLogDerivative.lean:184

theorem

Kadiri.kadiri_thm_3_1_q1_eq_12

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.Kadiri · PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:216

theorem

Kadiri.laplaceTransform_ibp

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.Kadiri · PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1631

theorem

Kadiri.kadiriTestFn_decay

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.Kadiri · PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2268

theorem

Kadiri.kadiriTestFn_laplaceTransform

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.Kadiri · PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2343

theorem

Kadiri.identity_16_complex_weighted

Weighted complex form of equation (16), derived from the explicit formula kadiri_thm_3_1_q1 at the Kadiri test function. The zero sum carries the multiplicities that the residue calculus produces; the set-sum form of identity_16_complex follows when every zero in the strip is simple. The two hypotheses are the explicit formula's convergence inputs, instantiated at the test function (dischargeable through the F₂(s-z)/(s-z)² representation).

PrimeNumberTheoremAnd.IEANTN.Kadiri · PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2495

theorem

Kadiri.laplaceTransform_re_decay

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.Kadiri · PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2726

theorem

Kadiri.laplaceTransform_sub_pole_norm_decay

Norm decay of the pole-subtracted Laplace transform on a right half-plane: subtracting the f 0 / s pole removes the only 1/|Im s|-order term of laplaceTransform_ibp, so the remainder F₂(s)/s² decays like 1/(Im s)^2 in norm, not just in real part. The full transform does NOT have this decay (its imaginary part is of order f 0 / Im s), which is why the complex sum ∑ ρ, F(s - ρ) over the zeta zeros is not absolutely summable for f 0 ≠ 0, while the pole-subtracted sum is.

PrimeNumberTheoremAnd.IEANTN.Kadiri · PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2833

theorem

Kadiri.summable_lap_sub_pole_at_zeros

Unconditional summability over the non-trivial zeros of the pole-subtracted Laplace transform. The un-subtracted complex sum ∑ ρ, F(s - ρ) is not absolutely summable when f 0 ≠ 0 (terms of norm ~ |f 0| / |Im ρ|); in equation (16) the groups f 0 * ∑ ρ, 1/(s - ρ) and -∑ ρ, F(s - ρ) combine into exactly this summand, which is O(1/(Im ρ)^2) and summable against the crude counting majorant.

PrimeNumberTheoremAnd.IEANTN.Kadiri · PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2911

theorem

Kadiri.summable_re_one_div_at_zeros

Unconditional summability of the real parts of the zero residues: Re (1/(s - ρ)) = Re (s - ρ) / |s - ρ|² decays like 1/(Im ρ)^2 on the strip, while the complex sum ∑ ρ, 1/(s - ρ) is only conditionally convergent. This is the summability needed to move Re inside the residue sum of equation (16).

PrimeNumberTheoremAnd.IEANTN.Kadiri · PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2951

theorem

Kadiri.summable_one_div_add_one_div_at_zeros

Summability of the genus-one zero packets 1/ρ + 1/(s - ρ): away from finitely many zeros the packet equals s/(ρ(s - ρ)), of norm at most ‖s‖/2 · (1/(Im ρ)² + 1/(Im (s - ρ))²) by AM-GM, and both square tails are summable by the crude counting majorant. This is the convergence input that makes the paired form of the residue sums legitimate.

PrimeNumberTheoremAnd.IEANTN.Kadiri · PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3004

theorem

Kadiri.re_tsum_paired_eq_re_inv_add_re_shifted

Distributing Re over the packet sum: the paired complex sum splits into the two absolutely summable real-part sums.

PrimeNumberTheoremAnd.IEANTN.Kadiri · PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3077

theorem

Kadiri.summable_kadiriTestFn_weighted_at_zeros

The explicit formula's weighted zero-sum hypothesis holds at the Kadiri test function: each integral is the pole-subtracted packet f 0/(s-ρ) - F(s-ρ), of norm O(1/(Im (s-ρ))²), and the order weight is carried by the unconditional weighted square tail. This discharges hΦ_sum of identity_16_complex_weighted.

PrimeNumberTheoremAnd.IEANTN.Kadiri · PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3112

theorem

Kadiri.summable_lap_re_at_zeros

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.Kadiri · PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3203

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.