Basic definitions and notation

DefinitionFirst prime gap#

\(P(g)\) is the first prime \(p_n\) for which the prime gap \(p_{n+1}-p_n\) is equal to \(g\), or \(0\) if no such gap exists.

Lean

Formalized as first_gap.

Sources
Leanfirst_gap

Definitionpi#

\(\pi(x)\) is the number of primes less than or equal to \(x\).

Lean

Formalized as pi.

Sources
Leanpi
Used by 2
Used byEquation (1) of FKS2 · pi star

Definitionpi star#

\(\pi^*(x) = \sum_{k \geq 1} \pi(x^{1/k}) / k\).

Lean

Formalized as pi_star.

Sources
Leanpi_star
Uses 1
Statement usespi

Definitionli and Li#

\(\mathrm{li}(x) = \int_0^x \frac{dt}{\log t}\) (in the principal value sense) and \(\mathrm{Li}(x) = \int_2^x \frac{dt}{\log t}\).

Lean

Formalized as li, Li.

Sources
Leanli · Li
Used by 1
Used byEquation (1) of FKS2

DefinitionEquation (2) of FKS2#

\(E_\psi(x) = |\psi(x) - x| / x\)

Lean

Formalized as Eψ.

Sources
LeanEψ
Used by 2
Used byDefinitions 1, 5, FKS2 · Classic bound implies numerical bound

DefinitionDefinitions 1, 5, FKS2#

We say that \(E_\psi\) satisfies a classical bound with parameters \(A, B, C, R, x_0\) if for all \(x \geq x_0\) we have

\[ E_\psi(x) \leq A \left(\frac{\log x}{R}\right)^B \exp\left(-C \left(\frac{\log x}{R}\right)^{1/2} \right). \]

We say that it obeys a numerical bound with parameter \(\varepsilon(x_0)\) if for all \(x \geq x_0\) we have

\[ E_\psi(x) \leq \varepsilon(x_0). \]
Lean

Formalized as Eψ.classicalBound.

Sources
LeanEψ.classicalBound
Uses 1 · Used by 1
Statement usesEquation (2) of FKS2
Used byClassic bound implies numerical bound

DefinitionEquation (1) of FKS2#

\(E_\pi(x) = |\pi(x) - \mathrm{Li}(x)| / (x / \log x)\).

Lean

Formalized as Eπ.

Sources
LeanEπ
Uses 2 · Used by 2
Statement usespi · li and Li
Used byDefinitions 1, 5, FKS2 · Classic bound implies numerical bound

DefinitionEquation (2) of FKS2#

\(E_\theta(x) = |\theta(x) - x| / x\)

Lean

Formalized as Eθ.

Sources
LeanEθ
Used by 2
Used byDefinitions 1, 5, FKS2 · Classic bound implies numerical bound

DefinitionDefinitions 1, 5, FKS2#

We say that \(E_\theta\) satisfies a classical bound with parameters \(A, B, C, R, x_0\) if for all \(x \geq x_0\) we have

\[ E_\theta(x) \leq A \left(\frac{\log x}{R}\right)^B \exp\left(-C \left(\frac{\log x}{R}\right)^{1/2} \right). \]

We say that it obeys a numerical bound with parameter \(\varepsilon(x_0)\) if for all \(x \geq x_0\) we have

\[ E_\theta(x) \leq \varepsilon(x_0). \]
Lean

Formalized as Eθ.classicalBound.

Sources
LeanEθ.classicalBound
Uses 1 · Used by 1
Statement usesEquation (2) of FKS2
Used byClassic bound implies numerical bound

DefinitionDefinitions 1, 5, FKS2#

We say that \(E_\pi\) satisfies a classical bound with parameters \(A, B, C, R, x_0\) if for all \(x \geq x_0\) we have

\[ E_\pi(x) \leq A \left(\frac{\log x}{R}\right)^B \exp\left(-C \left(\frac{\log x}{R}\right)^{1/2} \right). \]

We say that it obeys a numerical bound with parameter \(\varepsilon(x_0)\) if for all \(x \geq x_0\) we have

\[ E_\pi(x) \leq \varepsilon(x_0). \]
Lean

Formalized as Eπ.classicalBound.

Sources
LeanEπ.classicalBound
Uses 1 · Used by 1
Statement usesEquation (1) of FKS2
Used byClassic bound implies numerical bound

LemmaAdmissible bound decreasing for large x#

If \(A,B,C,R > 0\) then the classical bound is monotone decreasing for \(x \geq \exp( R (2B/C)^2 )\).

Proof

Differentiate the bound and check the sign.

Lean

Formalized as admissible_bound.mono.

Sources
Leanadmissible_bound.mono
Discussionhttps://github.com/AlexKontorovich/PrimeNumberTheoremAnd/issues/900
Used by 1
Used byClassic bound implies numerical bound

LemmaClassic bound implies numerical bound#

A classical bound for \(x \geq x_0\) implies a numerical bound for \(x \geq \max(x_0, \exp( R (2B/C)^2 ))\).

Proof

Immediate from previous lemma

Lean

Formalized as Eψ.classicalBound.to_numericalBound, Eθ.classicalBound.to_numericalBound, Eπ.classicalBound.to_numericalBound.

Sources
LeanEψ.classicalBound.to_numericalBound · Eθ.classicalBound.to_numericalBound · Eπ.classicalBound.to_numericalBound
Discussionhttps://github.com/AlexKontorovich/PrimeNumberTheoremAnd/issues/901
Uses 7
Statement usesEquation (2) of FKS2 · Definitions 1, 5, FKS2 · Definitions 1, 5, FKS2 · Equation (2) of FKS2 · Definitions 1, 5, FKS2 · Equation (1) of FKS2
Proof usesAdmissible bound decreasing for large x

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.