PrimeReciprocalInterval.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform reciprocal-prime mass on multiplicative intervals

theorem OAI.JointDickman.prime_reciprocal_interval_bound line 12
Source documentation
The proved Mertens remainder controls any prime interval by its multiplicative width and the logarithm of its lower endpoint.
```
theorem prime_reciprocal_interval_bound : ∃ C : ℝ, 0 ≤ C ∧
    ∀ L U R : ℝ, 2 ≤ L → L ≤ U → 1 ≤ R → U ≤ R*L →
      (∑ p ∈ largePrimeSet U L, 1/(p:ℝ)) ≤ (Real.log R+C)/Real.log L := by
…
```
Mentions: OAI.JointDickman.largePrimeSet

theorem OAI.JointDickman.prime_reciprocal_interval_subset line 52

Source documentation

The same bound for an arbitrary subset of such a prime interval.

theorem prime_reciprocal_interval_subset : ∃ C : ℝ, 0 ≤ C ∧
    ∀ (P : Finset ℕ) (L U R : ℝ), 2 ≤ L → 1 ≤ R → U ≤ R*L →
      (∀ p ∈ P, p.Prime ∧ L < (p:ℝ) ∧ (p:ℝ) ≤ U) →
      (∑ p ∈ P, 1/(p:ℝ)) ≤ (Real.log R+C)/Real.log L := by
…