OAI/NumberTheory/ShortEgyptian/SmoothBounds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ShortEgyptian.primeRecipBound line 10
  2. theorem OAI.ShortEgyptian.prime_reciprocals_real line 13
  3. theorem OAI.ShortEgyptian.shifted_prime_sum line 26
  4. def OAI.ShortEgyptian.smallSmoothConst line 45
  5. theorem OAI.ShortEgyptian.smallSmoothConst_nonneg line 47
  6. theorem OAI.ShortEgyptian.small_prime_sum line 50
  7. theorem OAI.ShortEgyptian.factored_primesLE line 67
  8. theorem OAI.ShortEgyptian.divisor_harmonic_bound line 74
  9. theorem OAI.ShortEgyptian.rough_exponential_bound line 91
  10. theorem OAI.ShortEgyptian.prefix_weight_bound line 107
  11. theorem OAI.ShortEgyptian.smooth_prefix_sum line 128
  12. theorem OAI.ShortEgyptian.small_smooth_prefix_sum line 141