Elementary Corollaries

Lemmafinsum-range-eq-sum-range#

For any arithmetic function \(f\) and real number \(x\), one has

\[ \sum_{n \leq x} f(n) = \sum_{n \leq ⌊x⌋_+} f(n) \]

and

\[ \sum_{n < x} f(n) = \sum_{n < ⌈x⌉_+} f(n). \]
Proof

Straightforward.

Lean

Formalized as finsum_range_eq_sum_range.

Sources
Leanfinsum_range_eq_sum_range

Theoremchebyshev-asymptotic#

One has

\[ \sum_{p \leq x} \log p = x + o(x). \]
Proof

From the prime number theorem we already have

\[ \sum_{n \leq x} \Lambda(n) = x + o(x) \]

so it suffices to show that

\[ \sum_{j \geq 2} \sum_{p^j \leq x} \log p = o(x). \]

Only the terms with \(j \leq \log x / \log 2\) contribute, and each \(j\) contributes at most \(\sqrt{x} \log x\) to the sum, so the left-hand side is \(O( \sqrt{x} \log^2 x ) = o(x)\) as required.

Lean

Formalized as chebyshev_asymptotic.

Sources
Leanchebyshev_asymptotic
Uses 1 · Used by 3
Proof usesWeakPNT
Used byPrime number theorem in AP · pi-asymp · primorial-bounds

Corollaryprimorial-bounds#

We have

\[ \prod_{p \leq x} p = \exp( x + o(x) ) \]
Proof

Exponentiate Theorem chebyshev_asymptotic.

Lean

Formalized as primorial_bounds.

Sources
Leanprimorial_bounds
Uses 1
Proof useschebyshev-asymptotic

Theorempi-asymp#

There exists a function \(c(x)\) such that \(c(x) = o(1)\) as \(x \to \infty\) and

\[ \pi(x) = (1 + c(x)) \int_2^x \frac{dt}{\log t} \]

for all \(x\) large enough.

Proof

We have the identity

\[ \pi(x) = \frac{1}{\log x} \sum_{p \leq x} \log p + \int_2^x (\sum_{p \leq t} \log p) \frac{dt}{t \log^2 t} \]

as can be proven by interchanging the sum and integral and using the fundamental theorem of calculus. For any \(\varepsilon\), we know from Theorem chebyshev_asymptotic that there is \(x_\varepsilon\) such that \(\sum_{p \leq t} \log p = t + O(\varepsilon t)\) for \(t \geq x_\varepsilon\), hence for \(x \geq x_\varepsilon\)

\[ \pi(x) = \frac{1}{\log x} (x + O(\varepsilon x)) + \int_{x_\varepsilon}^x (t + O(\varepsilon t)) \frac{dt}{t \log^2 t} + O_\varepsilon(1) \]

where the \(O_\varepsilon(1)\) term can depend on \(x_\varepsilon\) but is independent of \(x\). One can evaluate this after an integration by parts as

\[ \pi(x) = (1+O(\varepsilon)) \int_{x_\varepsilon}^x \frac{dt}{\log t} + O_\varepsilon(1) \]
\[ = (1+O(\varepsilon)) \int_{2}^x \frac{dt}{\log t} \]

for \(x\) large enough, giving the claim.

Lean

Formalized as pi_asymp.

Sources
Leanpi_asymp
Uses 1 · Used by 1
Proof useschebyshev-asymptotic
Used bypi-alt

Corollarypi-alt#

One has

\[ \pi(x) = (1+o(1)) \frac{x}{\log x} \]

as \(x \to \infty\).

Proof

An integration by parts gives

\[ \int_2^x \frac{dt}{\log t} = \frac{x}{\log x} - \frac{2}{\log 2} + \int_2^x \frac{dt}{\log^2 t}. \]

We have the crude bounds

\[ \int_2^{\sqrt{x}} \frac{dt}{\log^2 t} = O( \sqrt{x} ) \]

and

\[ \int_{\sqrt{x}}^x \frac{dt}{\log^2 t} = O( \frac{x}{\log^2 x} ) \]

and combining all this we obtain

\[ \int_2^x \frac{dt}{\log t} = \frac{x}{\log x} + O( \frac{x}{\log^2 x} ) \]
\[ = (1+o(1)) \frac{x}{\log x} \]

and the claim then follows from Theorem pi-asymp.

Lean

Formalized as pi_alt.

Sources
Leanpi_alt
Uses 1 · Used by 4
Proof usespi-asymp
Used bypn-asymptotic · prime-between · bound-score-2 · bound-score-3

Propositionpn-asymptotic#

One has

\[ p_n = (1+o(1)) n \log n \]

as \(n \to \infty\).

Proof

Use Corollary pi-alt to show that \(n=\pi(p_n)\sim p_n/\log p_n\) Taking logs gives \(\log n \sim \log p_n - \log\log p_n \sim \log p_n\). Multiplying these gives \(p_n\sim n\log n\) from which the result follows.

Lean

Formalized as pn_asymptotic.

Sources
Leanpn_asymptotic
Uses 1 · Used by 1
Proof usespi-alt
Used bypn-pn-plus-one

Corollarypn-pn-plus-one#

We have \(p_{n+1} - p_n = o(p_n)\) as \(n \to \infty\).

Proof

Easy consequence of preceding proposition.

Lean

Formalized as pn_pn_plus_one.

Sources
Leanpn_pn_plus_one
Uses 1
Proof usespn-asymptotic

Corollaryprime-between#

For every \(\varepsilon>0\), there is a prime between \(x\) and \((1+\varepsilon)x\) for all sufficiently large \(x\).

Proof

Use Corollary pi-alt to show that \(\pi((1+\varepsilon)x) - \pi(x)\) goes to infinity as \(x \to \infty\).

Lean

Formalized as prime_between.

Sources
Leanprime_between
Uses 1
Proof usespi-alt

Propositionmun#

We have \(|\sum_{n \leq x} \frac{\mu(n)}{n}| \leq 1\).

Proof

From Möbius inversion \(1_{n=1} = \sum_{d|n} \mu(d)\) and summing we have

\[ 1 = \sum_{d \leq x} \mu(d) \lfloor \frac{x}{d} \rfloor \]

for any \(x \geq 1\). Since \(\lfloor \frac{x}{d} \rfloor = \frac{x}{d} - \epsilon_d\) with \(0 \leq \epsilon_d < 1\) and \(\epsilon_x = 0\), we conclude that

\[ 1 ≥ x \sum_{d \leq x} \frac{\mu(d)}{d} - (x - 1) \]

and the claim follows.

Lean

Formalized as sum_mobius_div_self_le.

Sources
Leansum_mobius_div_self_le
Used by 2
Used bylambda-pnt · Möbius form of prime number theorem

PropositionMöbius form of prime number theorem#

We have \(\sum_{n \leq x} \mu(n) = o(x)\).

Proof

From the Dirichlet convolution identity

\[ \mu(n) \log n = - \sum_{d|n} \mu(d) \Lambda(n/d) \]

and summing we obtain

\[ \sum_{n \leq x} \mu(n) \log n = - \sum_{d \leq x} \mu(d) \sum_{m \leq x/d} \Lambda(m). \]

For any \(\varepsilon>0\), we have from the prime number theorem that

\[ \sum_{m \leq x/d} \Lambda(m) = x/d + O(\varepsilon x/d) + O_\varepsilon(1) \]

(divide into cases depending on whether \(x/d\) is large or small compared to \(\varepsilon\)). We conclude that

\[ \sum_{n \leq x} \mu(n) \log n = - x \sum_{d \leq x} \frac{\mu(d)}{d} + O(\varepsilon x \log x) + O_\varepsilon(x). \]

Applying Proposition mun we conclude that

\[ \sum_{n \leq x} \mu(n) \log n = O(\varepsilon x \log x) + O_\varepsilon(x). \]

and hence

\[ \sum_{n \leq x} \mu(n) \log x = O(\varepsilon x \log x) + O_\varepsilon(x) + O( \sum_{n \leq x} (\log x - \log n) ). \]

From Stirling's formula one has

\[ \sum_{n \leq x} (\log x - \log n) = O(x) \]

thus

\[ \sum_{n \leq x} \mu(n) \log x = O(\varepsilon x \log x) + O_\varepsilon(x) \]

and thus

\[ \sum_{n \leq x} \mu(n) = O(\varepsilon x) + O_\varepsilon(\frac{x}{\log x}). \]

Sending \(\varepsilon \to 0\) we obtain the claim.

Lean

Formalized as mu_pnt.

Sources
Leanmu_pnt
Uses 2 · Used by 2
Proof usesWeakPNT · mun
Used bylambda-pnt · Alternate Möbius form of prime number theorem

Propositionlambda-pnt#

We have \(\sum_{n \leq x} \lambda(n) = o(x)\).

Proof

From the identity

\[ \lambda(n) = \sum_{d^2|n} \mu(n/d^2) \]

and summing, we have

\[ \sum_{n \leq x} \lambda(n) = \sum_{d \leq \sqrt{x}} \sum_{n \leq x/d^2} \mu(n). \]

For any \(\varepsilon>0\), we have from Proposition Möbius form of prime number theorem that

\[ \sum_{n \leq x/d^2} \mu(n) = O(\varepsilon x/d^2) + O_\varepsilon(1) \]

and hence on summing in \(d\)

\[ \sum_{n \leq x} \lambda(n) = O(\varepsilon x) + O_\varepsilon(x^{1/2}). \]

Sending \(\varepsilon \to 0\) we obtain the claim.

Lean

Formalized as lambda_pnt.

Sources
Leanlambda_pnt
Uses 3
Proof usesWeakPNT · Möbius form of prime number theorem · mun

PropositionAlternate Möbius form of prime number theorem#

We have \(\sum_{n \leq x} \mu(n)/n = o(1)\).

Proof

As in the proof of Theorem mun, we have

\[ 1 = \sum_{d \leq x} \mu(d) \lfloor \frac{x}{d} \rfloor \]
\[ = x \sum_{d \leq x} \frac{\mu(d)}{d} - \sum_{d \leq x} \mu(d) \{ \frac{x}{d} \} \]

so it will suffice to show that

\[ \sum_{d \leq x} \mu(d) \{ \frac{x}{d} \} = o(x). \]

Let \(N\) be a natural number. It suffices to show that

\[ \sum_{d \leq x} \mu(d) \{ \frac{x}{d} \} = O(x/N). \]

if \(x\) is large enough depending on \(N\). We can split the left-hand side as the sum of

\[ \sum_{d \leq x/N} \mu(d) \{ \frac{x}{d} \} \]

and

\[ \sum_{j=1}^{N-1} \sum_{x/(j+1) < d \leq x/j} \mu(d) (x/d - j). \]

The first term is clearly \(O(x/N)\). For the second term, we can use Theorem Möbius form of prime number theorem and summation by parts (using the fact that \(x/d-j\) is monotone and bounded) to find that

\[ \sum_{x/(j+1) < d \leq x/j} \mu(d) (x/d - j) = o(x) \]

for any given \(j\), so in particular

\[ \sum_{x/(j+1) < d \leq x/j} \mu(d) (x/d - j) = O(x/N^2) \]

for all \(j=1,\dots,N-1\) if \(x\) is large enough depending on \(N\). Summing all the bounds, we obtain the claim.

Lean

Formalized as mu_pnt_alt.

Sources
Leanmu_pnt_alt
Uses 1
Proof usesMöbius form of prime number theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.