PrimeReciprocalBound.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.prime_reciprocal_dyadic_block line 10
Source documentation
A dyadic prime block contributes at most a constant divided by its logarithmic index. This uses only the elementary Chebyshev upper bound.
```
theorem prime_reciprocal_dyadic_block (n : ℕ) (hn : 1 ≤ n) :
    ∑ p ∈ Nat.primesLE (2 ^ (n + 1)) \ Nat.primesLE (2 ^ n),
      (1 : ℝ) / p ≤ 4 / (n : ℝ) := by
…
```
theorem OAI.Problem337.prime_reciprocal_two_pow line 67
Source documentation
Summing dyadic blocks gives a harmonic majorant for prime reciprocals.
```
theorem prime_reciprocal_two_pow (n : ℕ) :
    ∑ p ∈ Nat.primesLE (2 ^ n), (1 : ℝ) / p ≤ 8 * (harmonic n : ℝ) := by
…
```
theorem OAI.Problem337.prime_reciprocal_log_bound line 93
Source documentation
A direct logarithmic majorant, with the binary logarithm only in the argument of the outside logarithm.
```
theorem prime_reciprocal_log_bound (T : ℕ) :
    ∑ p ∈ Nat.primesLE T, (1 : ℝ) / p ≤
      8 * (1 + Real.log ((Nat.log 2 T + 1 : ℕ) : ℝ)) := by
…
```

theorem OAI.Problem337.sum_prime_reciprocals_le_loglog line 110

Source documentation

An elementary uniform O(log log T) bound for reciprocal primes.

theorem sum_prime_reciprocals_le_loglog (T : ℕ) (hT : 2 ≤ T) :
    ∑ p ∈ Nat.primesLE T, (1 : ℝ) / p ≤
      56 * Real.log (1 + Real.log (T : ℝ)) := by
…