OAI/NumberTheory/PrimeGaps/Indices.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargePrimeGaps.prime line 7

    Also declared: ComparatorChallenges/PrimeGaps.lean:7 (same declaration text).

  2. def OAI.LargePrimeGaps.largeGapIndices line 9

    Also declared: ComparatorChallenges/PrimeGaps.lean:9 (same declaration text).

  3. def OAI.LargePrimeGaps.primeIndex line 14
  4. def OAI.LargePrimeGaps.successor line 16
  5. theorem OAI.LargePrimeGaps.prime_isPrime line 18
  6. theorem OAI.LargePrimeGaps.prime_primeIndex line 21
  7. theorem OAI.LargePrimeGaps.primeIndex_pos line 24
  8. theorem OAI.LargePrimeGaps.primeIndex_prime line 27
  9. theorem OAI.LargePrimeGaps.prime_lt_prime line 30
  10. theorem OAI.LargePrimeGaps.prime_le_prime line 35
  11. theorem OAI.LargePrimeGaps.lt_successor line 40
  12. theorem OAI.LargePrimeGaps.successor_isPrime line 45
  13. theorem OAI.LargePrimeGaps.successor_le_of_prime_lt line 47
  14. def OAI.LargePrimeGaps.goodStarts line 56
  15. def OAI.LargePrimeGaps.gapPrimes line 62
  16. theorem OAI.LargePrimeGaps.exists_gapPrime_of_goodStart line 67
  17. theorem OAI.LargePrimeGaps.goodStarts_card_le line 96
  18. theorem OAI.LargePrimeGaps.primeIndex_injOn line 114
  19. theorem OAI.LargePrimeGaps.gapPrimes_card_le_largeGapIndices line 118
  20. theorem OAI.LargePrimeGaps.detector_cauchy line 144
  21. theorem OAI.LargePrimeGaps.mass_after_suppression line 164
  22. theorem OAI.LargePrimeGaps.mass_cauchy line 181
  23. theorem OAI.LargePrimeGaps.finite_moment_bound line 190
  24. def OAI.LargePrimeGaps.theta line 240
  25. def OAI.LargePrimeGaps.average line 242
  26. def OAI.LargePrimeGaps.detector line 245
  27. def OAI.LargePrimeGaps.blockLength line 248
  28. theorem OAI.LargePrimeGaps.log_pos_of_two_le line 251
  29. theorem OAI.LargePrimeGaps.theta_nonneg line 254
  30. theorem OAI.LargePrimeGaps.theta_pos_iff line 260
  31. theorem OAI.LargePrimeGaps.detector_nonneg line 266
  32. theorem OAI.LargePrimeGaps.detector_pos_iff line 270
  33. theorem OAI.LargePrimeGaps.one_le_detector line 276
  34. theorem OAI.LargePrimeGaps.first_detector_pos_iff line 287
  35. theorem OAI.LargePrimeGaps.second_detector_zero_iff line 301
  36. theorem OAI.LargePrimeGaps.goodStarts_eq_detector_filter line 321
  37. theorem OAI.LargePrimeGaps.goodStarts_bound_of_moments line 329
  38. theorem OAI.LargePrimeGaps.le_prime line 354
  39. theorem OAI.LargePrimeGaps.tendsto_prime line 359
  40. theorem OAI.LargePrimeGaps.primeCounting_prime line 362
  41. theorem OAI.LargePrimeGaps.eventually_index_log_prime_le line 369
  42. def OAI.LargePrimeGaps.indexScale line 378
  43. theorem OAI.LargePrimeGaps.tendsto_indexScale line 380
  44. theorem OAI.LargePrimeGaps.eventually_scale_comparison line 383
  45. theorem OAI.LargePrimeGaps.blockLength_le_mul_log line 409
  46. theorem OAI.LargePrimeGaps.eventually_blockLength_le line 413
  47. theorem OAI.LargePrimeGaps.eventually_blockLength_threshold line 428
  48. theorem OAI.LargePrimeGaps.index_bound_of_goodStarts line 444