bibkey: primenumbertheoremand2026medium authors: PrimeNumberTheoremAnd contributors year: 2026 title: PrimeNumberTheoremAnd – Medium prime number theorem doi: null url: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/tree/6a380f0c4658c04a420a9eb00b1ed62a1e3fde01 claim: The Chebyshev psi function has an error of order x times exp(-c (log x)^(1/10)) for some positive c, using compactly supported Mellin smoothing and contour estimates. strata_touched:

D5/S3/Weil/PrimeNumberTheorem/MellinCalculus
D5/S3/Weil/PrimeNumberTheorem/Smooth1
D5/S3/Weil/PrimeNumberTheorem/PntSmoothing
D5/S3/Weil/PrimeNumberTheorem/PntTail
D5/S3/Weil/PrimeNumberTheorem/PntLongVertical
D5/S3/Weil/PrimeNumberTheorem/PntShortContour
D5/S3/Weil/PrimeNumberTheorem/PntContourBound
D5/S3/Weil/PrimeNumberTheorem/MediumPNT license: Apache-2.0 triage: anchor

Medium prime number theorem

Locator

https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/tree/6a380f0c4658c04a420a9eb00b1ed62a1e3fde01

The immutable source tree contains PrimeNumberTheoremAnd/MellinCalculus.lean and PrimeNumberTheoremAnd/MediumPNT.lean, the consumed sources for the medium prime number theorem.

Source: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/tree/6a380f0c4658c04a420a9eb00b1ed62a1e3fde01

The immutable source uses Lean 4.32.2 and Mathlib 905b95818eb32af7874a58b427f50c1711a5e96c. Its consumed mathematical source is PrimeNumberTheoremAnd/MellinCalculus.lean and PrimeNumberTheoremAnd/MediumPNT.lean. The upstream tree contains the root LICENSE and no NOTICE file. Copyright the PrimeNumberTheoremAnd contributors.

The port has compactly supported Mellin convolution, smoothing kernels, Chebyshev vertical integrals, contour pieces, and twelve analytic declarations. It reuses the repository’s ZetaPntBase and ZetaPntBounds sources. This source distribution is modified from the cited source. The theorem’s logarithmic exponent is one tenth; it does not assert the optimal classical error exponent or an explicit value of its positive decay constant.

Retirement requires equivalent declarations in the Mathlib revision actually adopted by this repository, with direct applications preserving the original quantified contracts and standard axiom closure. At that point consumers use those declarations directly and the redundant local port is removed. An unadopted upstream revision or acceptance elsewhere does not meet this condition.

Mathematical contracts

The consumed definitions and bounds below are from the immutable PrimeNumberTheoremAnd source cited above. The corresponding local port is in D5/S3/Weil/PrimeNumberTheorem/; the exact statement types and proofs remain in those Lean modules. These are classical analytic inputs, not new theorems of the golden cubic block theory. Each displayed contract retains its own quantified hypotheses and parameters.

Mathematical conventions and definitions

Write $ζ$ for the ordinary Riemann zeta function, $ζ^{'}$ for its complex derivative, and

$ψ (X) = 1 \leq n \leq ⌊ X ⌋ \sum Λ (n),$

where $Λ$ is the von Mangoldt function; the sum is empty if its upper limit is less than one. Let $i^{2} = - 1$ . For a function $f$ on the positive real axis, its complex Mellin transform is

$M f (s) = \int_{0}^{\infty} x^{s - 1} f (x) d x .$

The real kernel is coerced into the complex numbers when the transform is applied to it. Support means the set where a function is nonzero. All set integrals in the contracts use Lebesgue measure; finite integrals $\int_{a}^{b}$ are oriented interval integrals. In Lean notation Icc, Ioo, Ioc, Iic, Ici, and uIcc mean closed, open, left-open right-closed, closed lower half-line, closed upper half-line, and unordered closed intervals, respectively. ContDiff ℝ 1 ν means that $ν$ is once continuously differentiable. HolomorphicOn f K means complex differentiability on $K$ , namely DifferentiableOn ℂ f K. The complex rectangle $[a,b]\times_{\mathbb C} [c,d]$ consists of complex numbers with real part in the first interval and imaginary part in the second.

For a complex-valued integrand $h$ , the normalized vertical integral used here is

$V^{'} (h, σ) = \frac{1}{2 πi} i \int_{R} h (σ + i t) d t .$

This is VerticalIntegral' h σ. The contour normalization and its orientation are part of every definition below; no unsigned path-length replacement is intended. The functions and predicates are defined for all displayed real parameters. Conditions such as $ϵ > 0$ , $X > 3$ , or unit mass are imposed only in the individual theorem that requires them. In particular, support does not silently imply nonnegativity, smoothness, or unit mass.

The exact definition fragments and theorem type fragments use the following notation. They specify mathematical contracts and are not standalone proof files.

open Set Function Filter Complex Real MeasureTheory ComplexConjugate Topology
open ArithmeticFunction (vonMangoldt)
open scoped Chebyshev ContDiff
local notation "𝓜" => mellin
local notation "Λ" => vonMangoldt
local notation "ζ" => riemannZeta
local notation "ζ'" => deriv ζ
variable {𝕂 : Type*} [RCLike 𝕂]

MellinConvolution. Multiplicative convolution of $f, g : R \to K$ , where $K$ is an RCLike scalar type, integrates $f (y) g (x / y)$ against $d y / y$ over $y > 0$ .

noncomputable def MellinConvolution (f g : ℝ → 𝕂) (x : ℝ) : 𝕂 :=
  ∫ y in Ioi 0, f y * g (x / y) / y

DeltaSpike. The dilation kernel associated with a real kernel $ν$ is $Δ_{ν, ϵ} (x) = ν (x^{1/ ϵ}) / ϵ$ . Its total real-power definition is the one displayed below; its analytic uses impose the required positive-parameter conditions.

noncomputable def DeltaSpike (ν : ℝ → ℝ) (ε : ℝ) : ℝ → ℝ :=
  fun x ↦ ν (x ^ (1 / ε)) / ε

Smooth1. The smoothed indicator $S_{ν, ϵ}$ is the multiplicative convolution of the indicator of $(0, 1]$ with $Δ_{ν, ϵ}$ .

noncomputable def Smooth1 (ν : ℝ → ℝ) (ε : ℝ) : ℝ → ℝ :=
  MellinConvolution (fun x ↦ if 0 < x ∧ x ≤ 1 then 1 else 0) (DeltaSpike ν ε)

SmoothedChebyshevIntegrand. For a real smoothing kernel $ν$ , write $h_{ν, ϵ, X} (s)$ for minus the logarithmic derivative of zeta times $M (S_{ν, ϵ}) (s) X^{s}$ . Complex powers and the coercion of the real smoothed indicator are exactly as displayed.

noncomputable abbrev SmoothedChebyshevIntegrand
    (SmoothingF : ℝ → ℝ) (ε : ℝ) (X : ℝ) : ℂ → ℂ :=
  fun s ↦ (- deriv riemannZeta s) / riemannZeta s *
    𝓜 (fun x ↦ (Smooth1 SmoothingF ε x : ℂ)) s * (X : ℂ) ^ s

SmoothedChebyshev. The smoothed Chebyshev reading is $V^{'} (h_{ν, ϵ, X}, 1 + (lo g X)^{- 1})$ , using the normalized vertical integral defined above.

noncomputable def SmoothedChebyshev (SmoothingF : ℝ → ℝ) (ε : ℝ) (X : ℝ) : ℂ :=
  VerticalIntegral' (SmoothedChebyshevIntegrand SmoothingF ε X) ((1 : ℝ) + (Real.log X)⁻¹)

I₁. $I_{1}$ is the lower infinite vertical tail on the line of real part $1 + (lo g X)^{- 1}$ , with imaginary parameter $t \leq - T$ .

noncomputable def I₁ (SmoothingF : ℝ → ℝ) (ε X T : ℝ) : ℂ :=
  (1 / (2 * π * I)) * (I * (∫ t : ℝ in Iic (-T),
      SmoothedChebyshevIntegrand SmoothingF ε X ((1 + (Real.log X)⁻¹) + t * I)))

I₂. $I_{2}$ is the horizontal piece at imaginary part $- T$ , oriented from real part $σ_{1}$ to $1 + (lo g X)^{- 1}$ .

noncomputable def I₂ (SmoothingF : ℝ → ℝ) (ε T X σ₁ : ℝ) : ℂ :=
  (1 / (2 * π * I)) * ((∫ σ in σ₁..(1 + (Real.log X)⁻¹),
    SmoothedChebyshevIntegrand SmoothingF ε X (σ - T * I)))

I₃₇. $I_{37}$ is the complete finite vertical piece on the line of real part $σ_{1}$ , oriented from imaginary part $- T$ to $T$ .

noncomputable def I₃₇ (SmoothingF : ℝ → ℝ) (ε T X σ₁ : ℝ) : ℂ :=
  (1 / (2 * π * I)) * (I * (∫ t in (-T)..T,
    SmoothedChebyshevIntegrand SmoothingF ε X (σ₁ + t * I)))

I₈. $I_{8}$ is the horizontal piece at imaginary part $T$ , oriented from real part $σ_{1}$ to $1 + (lo g X)^{- 1}$ .

noncomputable def I₈ (SmoothingF : ℝ → ℝ) (ε T X σ₁ : ℝ) : ℂ :=
  (1 / (2 * π * I)) * ((∫ σ in σ₁..(1 + (Real.log X)⁻¹),
    SmoothedChebyshevIntegrand SmoothingF ε X (σ + T * I)))

I₉. $I_{9}$ is the upper infinite vertical tail on the line of real part $1 + (lo g X)^{- 1}$ , with imaginary parameter $t \geq T$ .

noncomputable def I₉ (SmoothingF : ℝ → ℝ) (ε X T : ℝ) : ℂ :=
  (1 / (2 * π * I)) * (I * (∫ t : ℝ in Ici T,
      SmoothedChebyshevIntegrand SmoothingF ε X ((1 + (Real.log X)⁻¹) + t * I)))

I₃. $I_{3}$ is the lower finite vertical piece on the line of real part $σ_{1}$ , oriented from imaginary part $- T$ to $- 3$ .

noncomputable def I₃ (SmoothingF : ℝ → ℝ) (ε T X σ₁ : ℝ) : ℂ :=
  (1 / (2 * π * I)) * (I * (∫ t in (-T)..(-3),
    SmoothedChebyshevIntegrand SmoothingF ε X (σ₁ + t * I)))

I₇. $I_{7}$ is the upper finite vertical piece on the line of real part $σ_{1}$ , oriented from imaginary part $3$ to $T$ .

noncomputable def I₇ (SmoothingF : ℝ → ℝ) (ε T X σ₁ : ℝ) : ℂ :=
  (1 / (2 * π * I)) * (I * (∫ t in (3 : ℝ)..T,
    SmoothedChebyshevIntegrand SmoothingF ε X (σ₁ + t * I)))

I₄. $I_{4}$ is the short horizontal piece at imaginary part $- 3$ , oriented from real part $σ_{2}$ to $σ_{1}$ .

noncomputable def I₄ (SmoothingF : ℝ → ℝ) (ε X σ₁ σ₂ : ℝ) : ℂ :=
  (1 / (2 * π * I)) * ((∫ σ in σ₂..σ₁,
    SmoothedChebyshevIntegrand SmoothingF ε X (σ - 3 * I)))

I₆. $I_{6}$ is the short horizontal piece at imaginary part $3$ , oriented from real part $σ_{2}$ to $σ_{1}$ .

noncomputable def I₆ (SmoothingF : ℝ → ℝ) (ε X σ₁ σ₂ : ℝ) : ℂ :=
  (1 / (2 * π * I)) * ((∫ σ in σ₂..σ₁,
    SmoothedChebyshevIntegrand SmoothingF ε X (σ + 3 * I)))

I₅. $I_{5}$ is the central finite vertical piece on the line of real part $σ_{2}$ , oriented from imaginary part $- 3$ to $3$ .

noncomputable def I₅ (SmoothingF : ℝ → ℝ) (ε X σ₂ : ℝ) : ℂ :=
  (1 / (2 * π * I)) *
    (I * (∫ t in (-3)..3, SmoothedChebyshevIntegrand SmoothingF ε X (σ₂ + t * I)))

LogDerivZetaHasBound. The predicate $ZetaBound (A, C)$ requires $∣ ζ^{'} (σ + i t) / ζ (σ + i t) ∣ \leq C (lo g ∣ t ∣)^{9}$ for every real $σ, t$ with $3 < ∣ t ∣$ and $σ \geq 1 - A / (lo g ∣ t ∣)^{9}$ . It has no hidden upper bound on $σ$ .

def LogDerivZetaHasBound (A C : ℝ) : Prop := ∀ (σ : ℝ) (t : ℝ) (_ : 3 < |t|)
    (_ : σ ∈ Ici (1 - A / Real.log |t| ^ 9)), ‖ζ' (σ + t * I) / ζ (σ + t * I)‖ ≤
    C * Real.log |t| ^ 9

LogDerivZetaIsHoloSmall. The predicate $SmallHolo (σ_{2})$ requires the logarithmic derivative to be holomorphic on the unordered closed rectangle with real endpoints $σ_{2}, 2$ and imaginary endpoints $- 3, 3$ , with the point one removed.

def LogDerivZetaIsHoloSmall (σ₂ : ℝ) : Prop :=
    HolomorphicOn (fun (s : ℂ) ↦ ζ' s / (ζ s))
    (((uIcc σ₂ 2)  ×ℂ (uIcc (-3) 3)) \ {1})

Consumed analytic estimates

The following twelve clauses retain their own hypotheses independently. Their exact contracts are displayed to fix the quantifier order, parameter dependence, strict inequalities, orientations, and zero-free or holomorphic assumptions.

Vertical-strip Mellin decay. For every once continuously differentiable real kernel supported in [1/2, 2], one positive constant bounds its complex Mellin transform by that constant divided by the norm of the transform parameter. The bound applies uniformly when the real part is positive and at most two.