The prime number theorem, imported from PrimeNumberTheoremAnd

The normalisation step (Proposition 5.2 of the paper) needs the prime number theorem in the form θ(x) ~ x for Chebyshev's function θ. Mathlib does not contain it; the PrimeNumberTheoremAnd development already preserved in LeanPool.MooreBound does.

theorem Zeta5Irrational.theta_asymptotic : Asymptotics.IsEquivalent Filter.atTop Chebyshev.theta id

Chebyshev's function θ(x) = ∑_{p ≤ x} log p is asymptotic to x.