MertensScale.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The exact classical reciprocal-prime input and its sole required scale.

Published source: J. B. Rosser and L. Schoenfeld, Approximate formulas for some functions of prime numbers, Illinois J. Math. 6 (1962), 64–94, Theorem 5, (3.17)–(3.18), bounded-error consequence of Mertens' second theorem. DOI: https://doi.org/10.1215/ijm/1255631807. The bounded-error estimate controls the reciprocal-prime mass at the rough-sieve scale.

def OAI.TwoPointCorrelations.sievePrimesUpTo line 21
Also declared: OAI/NumberTheory/TwoPoint/Bounds/MertensScale.lean:21 (same declaration text).
def OAI.TwoPointCorrelations.PrimeReciprocalInput line 25
Source documentation
The bounded-error consequence of published Mertens' second theorem, with a uniform bound for all real cutoffs at least two.
Also declared: OAI/NumberTheory/TwoPoint/Bounds/MertensScale.lean:25 (same declaration text).
```
def PrimeReciprocalInput : Prop :=
…
```
lemma OAI.TwoPointCorrelations.sievePrimesUpTo_prime line 29
Also declared: OAI/NumberTheory/TwoPoint/Bounds/MertensScale.lean:29 (same declaration text).
lemma OAI.TwoPointCorrelations.sievePrimesUpTo_le line 32
Also declared: OAI/NumberTheory/TwoPoint/Bounds/MertensScale.lean:32 (same declaration text).
lemma OAI.TwoPointCorrelations.sievePrimesUpTo_card_le line 36
Also declared: OAI/NumberTheory/TwoPoint/Bounds/MertensScale.lean:36 (same declaration text).
theorem OAI.TwoPointCorrelations.PrimeReciprocalInput.rough_scale line 49
Source documentation
Precisely the prime reciprocal bounds used in the rough sieve, at y=exp(L^.99). The upper coefficient leaves room below 5/4.
Also declared: OAI/NumberTheory/TwoPoint/Bounds/MertensScale.lean:49 (same declaration text).
```
theorem PrimeReciprocalInput.rough_scale (hM : PrimeReciprocalInput) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ᶠ L : ℝ in atTop,
      (99 / 100 : ℝ) * Real.log L - C ≤
        ∑ p ∈ sievePrimesUpTo (Real.exp (L ^ (99 / 100 : ℝ))), 1 / (p : ℝ) ∧
      (∑ p ∈ sievePrimesUpTo (Real.exp (L ^ (99 / 100 : ℝ))), 1 / (p : ℝ)) ≤
        (5 / 4 : ℝ) * Real.log L := by
…
```
Mentions: OAI.TwoPointCorrelations.PrimeReciprocalInput, OAI.TwoPointCorrelations.sievePrimesUpTo