OAI/NumberTheory/Ostmann/Preliminaries/PrimeReciprocalBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

An elementary logarithmic bound for the reciprocal-prime sum

  1. theorem OAI.Ostmann.prime_dyadic_reciprocal_bound line 14
  2. theorem OAI.Ostmann.prime_reciprocal_sum_le_harmonic line 55
  3. theorem OAI.Ostmann.prime_reciprocal_sum_le_log line 82