MertensFromProgression.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Mertens estimates from the progression estimate

The conductor-one theta bound implies the first Mertens estimate.

theorem OAI.Ostmann.prime_log_div_partial_summation line 17

Source documentation

Abel summation for the logarithmically weighted prime sum.

theorem prime_log_div_partial_summation (Q : ℕ) (hQ : 2 ≤ Q) :
    (∑ p ∈ Nat.primesLE Q, Real.log (p : ℝ) / p) =
      Chebyshev.theta Q / Q + ∫ t in (2 : ℝ)..Q, Chebyshev.theta t / t ^ 2 := by
…

theorem OAI.Ostmann.theta_div_sq_integrable line 45

theorem OAI.Ostmann.PublishedProgressionInput.theta_error_integral line 59

Source documentation

The integrated theta error is bounded independently of the cutoff.

theorem PublishedProgressionInput.theta_error_integral (P : PublishedProgressionInput)
    (Q : ℕ) (hQ : 2 ≤ Q) :
    |∫ t in (2 : ℝ)..Q, (Chebyshev.theta t - t) / t ^ 2| ≤
      P.errorConstant * (-thetaErrorPrimitive P.decay 2) := by
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.thetaErrorPrimitive

def OAI.Ostmann.PublishedProgressionInput.mertensConstant line 102
theorem OAI.Ostmann.PublishedProgressionInput.mertensConstant_nonneg line 106
theorem OAI.Ostmann.PublishedProgressionInput.mertens line 115
Source documentation
First Mertens, with a concrete constant depending on the progression estimate.
```
theorem PublishedProgressionInput.mertens (P : PublishedProgressionInput) :
    MertensEstimate P.mertensConstant := by
…
```
Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.MertensEstimate