Partial sum of logarithm… to Integral form for second error…
LemmaPartial sum of logarithm identity#
For any \(x \geq 1\), one has
(NOTE: this identity is not actually needed in the proof of Mertens' theorems, but may be worth recording nevertheless.)
Proof
Apply the Euler-Maclaurin formula.
Lean
Formalized as Mertens.sum_log_eq.
Sources
LemmaPartial sum of logarithm upper bound#
For any \(x \geq 1\), one has
Proof
Trivial since \(\log n \leq \log x\).
Lean
Formalized as Mertens.sum_log_le.
Sources
Used by 1
CorollaryPartial sum of logarithm lower bound#
For any \(x \geq 1\), one has
Proof
We have
Here we use the monotonicity of \(\log n\) (and its vanishing at \(n=1\)) and the crude bound \(\log x \leq x\). Note: the tools at Mathlib.Analysis.SumIntegralComparisons may be useful.
Lean
Formalized as Mertens.sum_log_ge.
Sources
Used by 1
PropositionPartial sum of logarithm as logarithm of factorial#
For any \(x \geq 1\), one has
Proof
Follows from the definition of the factorial function. Is not needed for the Mertens theorems, but is a natural fact to have.
Lean
Formalized as Mertens.sum_log_eq_log_factorial.
Sources
LemmaPartial sum of logarithm as sum of \(\Lambda(d)/d\)#
For any real \(x\), one has
Proof
We have
Lean
Formalized as Mertens.sum_log_eq_sum_mangoldt.
Sources
DefinitionThe remainder term in Mertens first theorem (von Mangoldt form)#
We define \(E_{1,\Lambda}(x) := \sum_{d \leq x} \frac{\Lambda(d)}{d} - \log x\).
Lean
Formalized as Mertens.E₁Λ, Mertens.E₁Λ.bounded, Mertens.sum_mangoldt_div_eq_log'.
Sources
Used by 18
CorollaryPartial sum of \(\Lambda(d)/d\) lower bound#
For any \(x \geq 1\), one has
Proof
Insert Lemma Partial sum of logarithm as sum of \(\Lambda(d)/d\) into Lemma Partial sum of logarithm lower bound and lower bound \(x/d\) by \(\lfloor x/d \rfloor\).
Lean
Formalized as Mertens.E₁Λ.ge.
Sources
Uses 3 · Used by 5
CorollaryPartial sum of \(\Lambda(d)/d\) upper bound#
For any \(x \geq 1\), one has
Proof
Insert Lemma Partial sum of logarithm as sum of \(\Lambda(d)/d\) into Lemma Partial sum of logarithm upper bound and upper bound \(x/d\) by \(\lfloor x/d \rfloor + 1\), and use the Mathlib bound \(\psi(x) \leq (\log 4 + 4) x\).
Lean
Formalized as Mertens.E₁Λ.le.
Sources
Uses 3 · Used by 3
CorollaryMertens' first theorem (von Mangoldt form)#
For any \(x \geq 1\), one has
Proof
Immediate from previous two corollaries.
Lean
Formalized as Mertens.sum_mangoldt_div_eq_log.
Sources
DefinitionThe remainder term in Mertens first theorem (prime form)#
We define \(E_{1,p}(x) := \sum_{p \leq x} \frac{\log p}{p} - \log x\).
Used by 9
CorollaryPrime error for Mertens first theorem bounded by von Mangoldt error#
For any \(x \geq 1\), one has
Proof
Drop all terms in Lemma Partial sum of logarithm as sum of \(\Lambda(d)/d\) arising from prime powers.
Lean
Formalized as Mertens.E₁p.le_E₁Λ.
Sources
Uses 2 · Used by 1
CorollaryPartial sum of \(\frac{\log p}{p}\) upper bound#
For any \(x \geq 1\), one has
Proof
Drop all terms in Lemma Mertens-sum-mangoldt-div-le arising from prime powers.
Lean
Formalized as Mertens.E₁p.le.
Sources
Proposition\(E_1\) summable#
The series \(E_1 := \sum_p \frac{\log p}{p(p-1)}\) converges.
Proof
We have \(\sum_{n=2}^\infty \frac{\log n}{n(n-1)}\) converges by comparison with \(\sum_{n=2}^\infty \frac{2\log n}{n^2}\), which converges by the integral test. By a further application of comparison test we can conclude that \(E_1\) converges as well. Alternatively bound \(\log n\) by \(2\sqrt n\) and use the existing Mathlib API for \(\sum n^{-3/2}\).
Lean
Formalized as Mertens.E₁.summable.
Sources
Used by 2
PropositionUpper bound on \(E_1\)#
One has \(E_1 \leq \frac{5 \log 2 + 3}{4}\)
Proof
We can bound \(E_1 \leq \sum_{n=2}^\infty \frac{\log n}{n(n-1)} \leq \frac{\log 2}{2} + \frac{3}{2} \sum_{n=3}^\infty \frac{\log n}{n^2}\). Calculus shows that \(\log x / x^2\) is decreasing for \(x \geq 2 > e^{1/2}\), so we can bound \(\sum_{n=3}^\infty \frac{\log n}{n^2} \leq \int_2^\infty \frac{\log t}{t^2}\ dt = \frac{\log 2+1}{2}\).
Lean
Formalized as Mertens.E₁.le.
Sources
Uses 1 · Used by 1
CorollaryPartial sum of \(\frac{\log p}{p}\) lower bound#
For any \(x \geq 1\), one has
and thus
where
Proof
Use the triangle inequality and the geometric series formula to estimate in Lemma Mertens-sum-mangoldt-div-le arising from prime powers.
Lean
Formalized as Mertens.E₁Λ.le_E₁p_add_E₁.
Sources
Uses 3 · Used by 3
TheoremError term in Mertens' first theorem bounded (prime form)#
For any \(x \geq 1\), one has
Proof
Immediate from previous two corollaries.
Lean
Formalized as Mertens.sum_log_prime_div_eq_log, Mertens.sum_log_prime_div_eq_log'.
Sources
Uses 6 · Used by 4
DefinitionAlternate Formula for Euler-Mascheroni constant#
We set \(\gamma := \int_2^\infty \frac{E_{1,\Lambda}(t)}{t \log^2 t} \, dt + 1 - \log \log 2\).
Uses 1 · Used by 9
DefinitionThe remainder term in Mertens second theorem (von Mangoldt form)#
We define \(E_{2,\Lambda}(x) := \sum_{d \leq x} \frac{\Lambda(d)}{d \log d} - \log \log x - \gamma\).
Uses 2 · Used by 11
LemmaIntegral identity involving inverse log weight#
For any \(x \geq 2\) and any \(f : {\mathbb N} \mapsto {\mathbb R}\), one has
Proof
Establish the identity
for \(2 \leq n \leq x\),multiply by \(f(n)\), then sum.
Lean
Formalized as _private.PrimeNumberTheoremAnd.IEANTN.Mertens.0.Mertens.sum_div_log_eq.
Sources
CorollaryIntegral form for second error (von Mangoldt form)#
For any \(x \geq 2\), one has
Proof
From Lemma Integral identity involving inverse log weight one has
Now substitute the definitions of \(E_{1,\Lambda}\), \(E_{2,\Lambda}\), \(\gamma\) and simplify.
Lean
Formalized as Mertens.E₂Λ.eq.
Sources
Uses 5 · Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.