MRTPrimeBands.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Prime-band reciprocal masses used in MRT's typical-factorization sieve. The only classical input here is the already discharged Mertens theorem.

def OAI.TwoPointCorrelations.mrtPrimeBand line 14
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeBands.lean:14 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_sievePrimesUpTo_mono line 17
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeBands.lean:17 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtPrimeBand_prime line 23
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeBands.lean:23 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtPrimeBand_bounds line 26
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeBands.lean:26 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtPrimeBand_mass line 36
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeBands.lean:36 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_prime_band_mertens line 43
Source documentation
Uniform bounded-error reciprocal mass for every positive prime band.
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeBands.lean:43 (same declaration text).
```
theorem mrt_prime_band_mertens : ∃ C : ℝ, 0 ≤ C ∧
    ∀ P Q : ℝ, 2 ≤ P → P ≤ Q →
      |(∑ p ∈ mrtPrimeBand P Q, 1 / (p : ℝ)) -
        (Real.log (Real.log Q) - Real.log (Real.log P))| ≤ C := by
…
```
Mentions: OAI.TwoPointCorrelations.mrtPrimeBand
theorem OAI.TwoPointCorrelations.mrt_prime_band_product line 61
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeBands.lean:61 (same declaration text).