OAI/NumberTheory/PrimeGaps/ProfileSymmetry.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargePrimeGaps.cumulative_square_limit line 27
  2. theorem OAI.LargePrimeGaps.cumulative_cross_limit line 51
  3. theorem OAI.LargePrimeGaps.orderedWeight_second_limit line 67
  4. theorem OAI.LargePrimeGaps.cumulativeProfile_perm_orthant line 104
  5. theorem OAI.LargePrimeGaps.divisorSum_perm_orthant line 140
  6. def OAI.LargePrimeGaps.subsetEnumeration line 161
  7. theorem OAI.LargePrimeGaps.subsetEnumeration_image line 165
  8. def OAI.LargePrimeGaps.enumeratePerm line 178
  9. theorem OAI.LargePrimeGaps.enumeratePerm_image line 183
  10. theorem OAI.LargePrimeGaps.enumeratePerm_bijective line 196
  11. def OAI.LargePrimeGaps.unorderedBlock line 222
  12. theorem OAI.LargePrimeGaps.weightedBlock_eq_unordered line 227
  13. def OAI.LargePrimeGaps.unorderedWeight line 257
  14. theorem OAI.LargePrimeGaps.orderedWeight_eq_unordered line 262
  15. theorem OAI.LargePrimeGaps.unorderedWeight_second_limit line 271
  16. theorem OAI.LargePrimeGaps.unorderedWeight_fourth_bound line 282
  17. def OAI.LargePrimeGaps.separatedOffsets line 292
  18. theorem OAI.LargePrimeGaps.separatedBox_mem line 295
  19. def OAI.LargePrimeGaps.separatedBoxEquiv line 328
  20. theorem OAI.LargePrimeGaps.separated_double_sum line 345
  21. theorem OAI.LargePrimeGaps.pattern_marked_sum_eq_box line 356
  22. theorem OAI.LargePrimeGaps.separatedOffsets_eventually line 376
  23. theorem OAI.LargePrimeGaps.marked_pattern_limit line 383
  24. def OAI.LargePrimeGaps.orderedDetector line 403
  25. theorem OAI.LargePrimeGaps.average_div line 406
  26. theorem OAI.LargePrimeGaps.markedBlock_average_expansion line 410
  27. theorem OAI.LargePrimeGaps.markedBlock_average_limit line 433
  28. theorem OAI.LargePrimeGaps.marked_cumulative_pair_limit line 476
  29. theorem OAI.LargePrimeGaps.marked_cumulative_square_limit line 520
  30. theorem OAI.LargePrimeGaps.marked_cumulative_cross_limit line 533