MertensFromFirst.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The bounded second Mertens estimate from the first

Only bounded error is needed in the Ostmann application. Partial summation therefore makes the second prime-sum input a consequence of the first.

theorem OAI.Ostmann.MertensEstimate.floor_error line 18
def OAI.Ostmann.logPrimeCoefficient line 35
theorem OAI.Ostmann.sum_logPrimeCoefficient line 38
theorem OAI.Ostmann.sum_inv_log_mul_logPrimeCoefficient line 44
theorem OAI.Ostmann.inv_log_differentiable line 57
theorem OAI.Ostmann.inv_log_deriv_continuous line 61

theorem OAI.Ostmann.prime_reciprocal_partial_summation line 67

Source documentation

Partial summation for precisely the two prime weights used downstream.

theorem prime_reciprocal_partial_summation (Q : ℕ) (hQ : 2 ≤ Q) :
    (∑ p ∈ Nat.primesLE Q, (p : ℝ)⁻¹) =
      (∑ p ∈ Nat.primesLE Q, Real.log (p : ℝ) / p) / Real.log Q +
      ∫ t in (2 : ℝ)..Q,
        (∑ p ∈ Nat.primesLE ⌊t⌋₊, Real.log (p : ℝ) / p) *
          (t⁻¹ / Real.log t ^ 2) := by
…

theorem OAI.Ostmann.mertens_kernel_continuous line 91
theorem OAI.Ostmann.mertens_weighted_sum_integrable line 95
theorem OAI.Ostmann.mertens_log_kernel_continuous line 105
theorem OAI.Ostmann.mertens_log_kernel_integral line 110
theorem OAI.Ostmann.mertens_error_integral_bound line 122
theorem OAI.Ostmann.MertensEstimate.harmonic line 169
Source documentation
The bounded-error second theorem follows from the first; no second independent Mertens hypothesis is needed by the conditional main theorem.
```
theorem MertensEstimate.harmonic {C : ℝ} (hM : MertensEstimate C) :
    MertensHarmonicEstimate
      (|1 - Real.log (Real.log 2)| + (2 * C + Real.log 2) / Real.log 2) := by
…
```
Mentions: OAI.Ostmann.MertensEstimate, OAI.Ostmann.MertensHarmonicEstimate