OAI/NumberTheory/PrimeGaps/SingularTails.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargePrimeGaps.singularTailFactor line 13
  2. def OAI.LargePrimeGaps.singularTail line 16
  3. theorem OAI.LargePrimeGaps.singularTailFactor_pos line 19
  4. theorem OAI.LargePrimeGaps.singularTail_log_summable_bound line 27
  5. theorem OAI.LargePrimeGaps.singularTail_pos_and_log_bound line 45
  6. theorem OAI.LargePrimeGaps.singularTail_error line 54
  7. theorem OAI.LargePrimeGaps.singularSeries_eq_truncation_mul_tail line 62
  8. def OAI.LargePrimeGaps.siftedCount line 85
  9. def OAI.LargePrimeGaps.normalizedSiftedCount line 88
  10. theorem OAI.LargePrimeGaps.unit_indicator_sum line 91
  11. theorem OAI.LargePrimeGaps.shifted_unit_indicator_sum line 108
  12. theorem OAI.LargePrimeGaps.siftedCount_sum line 114
  13. theorem OAI.LargePrimeGaps.normalizedSiftedCount_sum line 130
  14. theorem OAI.LargePrimeGaps.siftedCount_crt line 141
  15. theorem OAI.LargePrimeGaps.normalizedSiftedCount_crt line 178
  16. theorem OAI.LargePrimeGaps.product_indicator line 187
  17. theorem OAI.LargePrimeGaps.siftedCount_prime line 196
  18. theorem OAI.LargePrimeGaps.normalizedSiftedCount_prime line 211
  19. def OAI.LargePrimeGaps.siftedTuple line 224
  20. theorem OAI.LargePrimeGaps.siftedTuple_eq line 229
  21. theorem OAI.LargePrimeGaps.siftedTuple_crt line 233
  22. theorem OAI.LargePrimeGaps.siftedTuple_one line 240
  23. theorem OAI.LargePrimeGaps.siftedTuple_product line 248
  24. theorem OAI.LargePrimeGaps.siftedCount_nonneg line 268
  25. theorem OAI.LargePrimeGaps.siftedCount_le line 273
  26. theorem OAI.LargePrimeGaps.normalizedSiftedCount_nonneg line 284
  27. theorem OAI.LargePrimeGaps.normalizedSiftedCount_le line 288
  28. theorem OAI.LargePrimeGaps.residueCount_eq_card_zmod line 300
  29. theorem OAI.LargePrimeGaps.siftedTuple_prime_eq line 319
  30. theorem OAI.LargePrimeGaps.siftedTuple_primorial_eq line 328
  31. def OAI.LargePrimeGaps.rangeResidue line 333
  32. theorem OAI.LargePrimeGaps.rangeResidue_card_bounds line 335
  33. def OAI.LargePrimeGaps.cyclicFiber line 365
  34. theorem OAI.LargePrimeGaps.cyclicFiber_card_bounds line 368
  35. def OAI.LargePrimeGaps.residueTuple line 393
  36. theorem OAI.LargePrimeGaps.residueTuple_fiber_card line 396
  37. theorem OAI.LargePrimeGaps.residueTuple_sum_bounds line 407
  38. def OAI.LargePrimeGaps.boxTuple line 444
  39. theorem OAI.LargePrimeGaps.boxTuple_collision_count line 447
  40. theorem OAI.LargePrimeGaps.boxTuple_nondistinct_count line 473