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 561 to 580 of 1,644 declarations.

theorem

Kadiri.identity_16

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

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

theorem

Kadiri.re_inner_eq

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

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

theorem

Kadiri.eq_5

Δ2(s):=T2(s)−κT2(s+δ)\Delta_2(s) := T_2(s) - \kappa T_2(s + \delta) - the difference operator applied to T2T_2. -/ noncomputable def Δ2 (f : ℝ → ℝ) (κ δ : ℝ) (s : ℂ) : ℝ := T2 f s - κ * T2 f (s + (δ : ℂ))

/-! ## Equation (5) of Kadiri2005: the "damped" explicit formula

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

lemma

Kadiri.tsum_vonMangoldt_neg_mellin_line

Collapse the von Mangoldt Dirichlet series on the negative Mellin line.

PrimeNumberTheoremAnd.IEANTN.KadiriEq11Reduction · PrimeNumberTheoremAnd/IEANTN/KadiriEq11Reduction.lean:94

lemma

Kadiri.kadiri_thm_3_1_q1_eq_11_summed_pv_of_pointwise_inversion_bound

Tannery exchange for the principal-value inversion terms. This converts pointwise PV inversion at each integer into the summed PV limit, using an explicit summable domination bound over n.

PrimeNumberTheoremAnd.IEANTN.KadiriEq11Reduction · PrimeNumberTheoremAnd/IEANTN/KadiriEq11Reduction.lean:454

theorem

Kadiri.kadiri_thm_3_1_q1_eq_11_pv_of_pointwise_inversion_bound

Principal-value reduction of Kadiri equation (11) from pointwise PV inversion and an explicit Tannery domination bound. The finite-window sum/integral exchange is proved in this file, and the final vertical-line reflection is the Dirichlet-series identity followed by t ↦ -t.

PrimeNumberTheoremAnd.IEANTN.KadiriEq11Reduction · PrimeNumberTheoremAnd/IEANTN/KadiriEq11Reduction.lean:565

theorem

Kadiri.kadiri_thm_3_1_q1_eq_11_pv_of_pointwise_inversion_tannery_bound

Principal-value reduction with the explicit Tannery majorant expected from the finite-height inversion bound. The only domination input is the eventual uniform estimate by a constant multiple of the absolutely summable von Mangoldt line Λ n / n^(1+a).

PrimeNumberTheoremAnd.IEANTN.KadiriEq11Reduction · PrimeNumberTheoremAnd/IEANTN/KadiriEq11Reduction.lean:628

theorem

Kadiri.kadiri_thm_3_1_q1_eq_11_pv_of_pointwise_inversion

Principal-value reduction of Kadiri equation (11) from pointwise PV inversion. The Tannery domination bound is discharged from the Kadiri decay hypotheses via the finite-window Fourier/Laplace estimate.

PrimeNumberTheoremAnd.IEANTN.KadiriEq11Reduction · PrimeNumberTheoremAnd/IEANTN/KadiriEq11Reduction.lean:675

theorem

Kadiri.kadiri_thm_3_1_q1_eq_11_of_inversion

Reduction of Kadiri equation (11) from the pointwise inversion identity.

The analytic exchange of the von Mangoldt sum with the Mellin integral is kept as an explicit hypothesis. This isolates the part blocked by the concrete Fubini/Tonelli side-condition proof while avoiding any dependency on the sorried inversion theorem in Kadiri.lean.

PrimeNumberTheoremAnd.IEANTN.KadiriEq11Reduction · PrimeNumberTheoremAnd/IEANTN/KadiriEq11Reduction.lean:715

theorem

Kadiri.kadiri_thm_3_1_q1_pointwise_inversion

The single-point truncated-limit inverse Laplace identity at y = log n (\cite{Kadiri2005}, the displayed equation just before eq.~(11)): for φ of class C¹ with the strip decay of (B), and any 0 < a < b with n ≥ 1,

= \lim_{T \to \infty} \frac{1}{2\pi i} \int_{-(1+a)-iT}^{-(1+a)+iT} \Phi(s)\, n^{s}\, ds,$$ with `Φ(s) = ∫ y, φ y e^{-s y}`. This is the truncated-window Fourier/Laplace inversion theorem from `PrimeNumberTheoremAnd.LaplaceInversion`, specialized to the contour `σ = -(1+a)` and the point `x = n` (so `n^s = exp (s log n)`). It discharges the `hinv` hypothesis carried by the eq.~(11) reduction lemmas above.

PrimeNumberTheoremAnd.IEANTN.KadiriEq11Reduction · PrimeNumberTheoremAnd/IEANTN/KadiriEq11Reduction.lean:812

theorem

Kadiri.kadiri_thm_3_1_q1_eq_11_truncated_limit_of_pointwise_inversion

The faithful truncated-limit form of Kadiri equation (11) (\cite{Kadiri2005}, Théorème 3.1, eq.~(11), arXiv math/0401238): the von Mangoldt sum is the T → ∞ limit of the truncated contour integral kadiri_thm_3_1_q1_I φ a T over the compact segment [1+a-iT, 1+a+iT]. Under the same C¹ hypotheses as the stub kadiri_thm_3_1_q1_eq_11, the only remaining analytic input is the single-point truncated-limit Laplace inversion hinv (the displayed identity just before \cite[(11)]{Kadiri2005}); the sum/integral exchange over the compact window and the Tannery domination are discharged by this file, so no full-line L¹ integrability is needed. This replaces the (mis-stated) absolute Bochner form ∫ t : ℝ of the stub.

PrimeNumberTheoremAnd.IEANTN.KadiriEq11Reduction · PrimeNumberTheoremAnd/IEANTN/KadiriEq11Reduction.lean:880

theorem

deriv_zpow_mul_eventuallyEq

If f = (z-x)^n • g near x (punctured) with g analytic, then deriv f is (z-x)^(n-1) • (n • g + (z-x) • g') near x.

PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:25

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.