PrimeReciprocalTheorem.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Mertens' second theorem in bounded-error form.

The formal proof uses Erdos970.Mertens.sum_prime_div_eq_log_log. Only the convention for the finite prime set differs from PrimeReciprocalInput; zero contributes no prime to either convention.

lemma OAI.TwoPointCorrelations.sievePrimesUpTo_eq_Ioc line 17
Also declared: OAI/NumberTheory/TwoPointCorrelations/PrimeReciprocalTheorem.lean:15 (same declaration text).
theorem OAI.TwoPointCorrelations.primeReciprocalInput line 28
Source documentation
Mertens' second theorem implies the reciprocal-prime estimate.
Also declared: OAI/NumberTheory/TwoPointCorrelations/PrimeReciprocalTheorem.lean:26 (same declaration text).
```
theorem primeReciprocalInput : PrimeReciprocalInput := by
…
```
Mentions: OAI.TwoPointCorrelations.PrimeReciprocalInput