OAI/NumberTheory/ShortEgyptian/DivisorWeights.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ShortEgyptian.momentSeriesConst line 10
  2. theorem OAI.ShortEgyptian.summable_shifted_geom line 13
  3. theorem OAI.ShortEgyptian.polynomial_geom_local line 24
  4. def OAI.ShortEgyptian.divisorWeight line 49
  5. theorem OAI.ShortEgyptian.divisorWeight_one line 52
  6. theorem OAI.ShortEgyptian.divisorWeight_mul line 55
  7. theorem OAI.ShortEgyptian.divisorWeight_prime_pow line 61
  8. theorem OAI.ShortEgyptian.prime_rpow_small line 71
  9. theorem OAI.ShortEgyptian.divisorWeight_prime_summable line 88
  10. theorem OAI.ShortEgyptian.smooth_divisor_weight line 96
  11. theorem OAI.ShortEgyptian.momentSeriesConst_nonneg line 123
  12. theorem OAI.ShortEgyptian.rankin_divisor_weight line 126