Bound for second Mertens error… to Mertens' third theorem error…
CorollaryBound for second Mertens error (von Mangoldt form)#
For any \(x \geq 2\), one has
Proof
Insert Lemma Partial sum of \(\Lambda(d)/d\) upper bound and Lemma Partial sum of \(\Lambda(d)/d\) lower bound into Lemma Integral form for second error (von Mangoldt form) and use the triangle inequality to obtain the required upper and lower bounds.
Lean
Formalized as Mertens.E₂Λ.abs_le, Mertens.E₂Λ.bound, Mertens.E₂Λ.bound'.
Sources
LemmaDirichlet series for \(\log \zeta(s)\)#
If \(s > 1\) then \(\log\zeta(s) = - \log (s-1) + \Gamma'(1) + \gamma + (s-1) \int_1^\infty E_{2,\Lambda}(x) x^{-s}\ ds\).
Proof
First use the fundamental theorem of calculus and decay of \(\log \zeta(s)\) to write
Then substitute in the known identity \(-\frac{\zeta'(u)}{\zeta(u)} = \sum_n \frac{\Lambda(n)}{n^u}\) and integrate term by term.
Lean
Formalized as Mertens.log_zeta_eq_sum.
Sources
Used by 1
LemmaIntegration by parts identity for \(\log \zeta(s)\)#
If \(s > 1\) then \(\log\zeta(s) = (s-1) \int_1^\infty (\log \log x + \gamma + E_{2,\Lambda}(x)) x^{-s})\ dx\).
Proof
Apply the preceding identity then integrate by parts.
Lean
Formalized as _private.PrimeNumberTheoremAnd.IEANTN.Mertens.0.Mertens.log_zeta_eq_integ.
Sources
Uses 4 · Used by 1
LemmaFirst integral identity#
If \(s > 1\) then \((s-1) \int_1^\infty \log \log x \cdot x^{-s}\ dx = -\log (s-1) + \Gamma'(1)\).
Proof
Writing \(t = \log x\), the LHS is \((s-1) \int_0^\infty \log t e^{-(s-1) t}\ dt\). Now differentiate \(\Gamma(z) = (s-1)^z \int_0^\infty t^{z-1} e^{-(s-1)t}\ dt\) in \(z\) at \(z=1\).
Lean
Formalized as _private.PrimeNumberTheoremAnd.IEANTN.Mertens.0.Mertens.mul_integ_log_log_eq.
Sources
Used by 1
LemmaSecond integral identity#
If \(s > 1\) then \((s-1) \int_1^\infty \gamma \cdot x^{-s}\ dx = \gamma\).
Proof
Apply the fundamental theorem of calculus.
Lean
Formalized as _private.PrimeNumberTheoremAnd.IEANTN.Mertens.0.Mertens.mul_integ_gamma_eq.
Sources
Uses 1 · Used by 1
TheoremAn identity for \(\log \zeta(s)\)#
If \(s > 1\) then \(\log\zeta(s) = - \log (s-1) + \Gamma'(1) + \gamma + (s-1) \int_1^\infty E_{2,\Lambda}(x) x^{-s}\ ds\).
Proof
Combine the previous four sublemmas.
Lean
Formalized as _private.PrimeNumberTheoremAnd.IEANTN.Mertens.0.Mertens.log_zeta_eq.
Sources
Uses 7 · Used by 1
Lemmalimiting behavior of log zeta#
One has \(\log \zeta(s) = - \log(s-1) + o(1)\) as \(s \to 1^+\).
Proof
Start with the asymptotic \(\zeta(s) = \frac{1}{s-1} + O(1)\) and take logarithms.
Lean
Formalized as _private.PrimeNumberTheoremAnd.IEANTN.Mertens.0.Mertens.log_zeta_limit.
Sources
Used by 1
TheoremCompatibility with Mathlib Euler-Mascheroni constant#
\(\gamma\) is the Euler–Mascheroni constant.
Proof
Take limits as \(s \to 1\) in the previous asymptotic using known asymptotics for \(\zeta(s)\), and using that \(- \Gamma'(1)\) is the Euler–Mascheroni constant.
Lean
Formalized as Mertens.deriv_gamma_add_γ_eq_zero.
Sources
Uses 6 · Used by 2
TheoremMertens' second theorem (weak von Mangoldt form)#
For any \(x \geq 2\), one has
Proof
Immediate from previous two corollaries.
Lean
Formalized as Mertens.sum_mangoldt_div_log_eq_log_log, Mertens.sum_mangoldt_div_log_eq_log_log'.
Sources
Uses 5
DefinitionThe Meissel-Mertens constant#
We define \(M := \int_2^\infty \frac{E_{1,p}(t)}{t \log^2 t} \, dt + 1 - \log \log 2\).
Uses 1 · Used by 7
CorollaryUpper bound for \(M\)#
One has \(M \leq \frac{\log 4 + 4}{\log 2} + 1 - \log \log 2\).
Proof
Insert Lemma Partial sum of \(\frac{\log p}{p}\) upper bound into the definition of \(M\) and use the fact that \(\int_2^\infty \frac{dt}{t \log^2 t} = 1/\log 2\).
Lean
Formalized as Mertens.M.le.
Sources
CorollaryLower bound for \(M\)#
One has \(M \geq -\frac{2 + E_1}{\log 2} + 1 - \log \log 2\).
Proof
Insert Lemma Partial sum of \(\frac{\log p}{p}\) lower bound into the definition of \(M\) and use the fact that \(\int_2^\infty \frac{dt}{t \log^2 t} = 1/\log 2\).
Lean
Formalized as Mertens.M.ge.
Sources
Uses 6
CorollaryIntegral form for second error (prime 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,p}\), \(E_{2,p}\), \(M\) and simplify.
Lean
Formalized as Mertens.E₂p.eq.
Sources
Uses 5 · Used by 1
CorollaryBound for second error (prime form)#
For any \(x \geq 2\), one has
Proof
Similar to Lemma Integral form for second error (prime form).
Lean
Formalized as Mertens.E₂p.abs_le, Mertens.E₂p.bound, Mertens.E₂p.bound'.
Sources
Uses 8 · Used by 3
TheoremMertens' second theorem (weak prime form)#
For any \(x \geq 2\), one has
Proof
Immediate from previous two corollaries.
Lean
Formalized as Mertens.sum_prime_div_eq_log_log, Mertens.sum_prime_div_eq_log_log'.
Sources
TheoremFormula for Meissel-Mertens constant#
One has \(M = \gamma + \sum_p \log(1-\frac{1}{p}) + \frac{1}{p}\).
Proof
The RHS can be Taylor expanded as \(\sum_{j=2}^\infty \sum_p \frac{1}{jp^j}\). Meanwhile, the difference between \(\sum_{n \leq x} \frac{\Lambda(n)}{n \log n}\) and \(\sum_{p \leq x} \frac{1}{p}\) is equal to \(\sum_{j=2}^\infty \sum_{p: p^j \leq x} \frac{1}{j p^j}\). Applying the monotone convergence theorem, Lemma Bound for second error (prime form), and Lemma Bound for second Mertens error (von Mangoldt form) gives the claim.
Lean
Formalized as Mertens.M.eq.
Sources
DefinitionThe remainder term in Mertens third theorem#
We define \(E_3(x) := \sum_{p \leq x} \log (1 - \frac{1}{p}) + \log\log x + \gamma\).
Used by 2
TheoremMertens' third theorem error term#
For any \(x \geq 2\), one has
Proof
Immediate from definition
Lean
Formalized as Mertens.prod_one_minus_div_prime_eq.
Sources
Uses 1 · Used by 1
TheoremMertens' third theorem error bound#
For any \(x \geq 2\), one has
Proof
Estimating the error in Formula for Meissel-Mertens constant using the first order Taylor expansion of log one gets
The result follows by combining with Bound for second error (prime form).
Lean
Formalized as Mertens.E₃.abs_le, Mertens.E₃.bound, Mertens.E₃.bound', Mertens.E₃.bound'''.
Sources
Uses 9
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.