OAI/NumberTheory/PrimeGaps/PairedDetectors.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargePrimeGaps.tensorProfile_extendPerm line 27
  2. def OAI.LargePrimeGaps.extendLabels line 35
  3. theorem OAI.LargePrimeGaps.extendLabels_left line 38
  4. theorem OAI.LargePrimeGaps.extendLabels_right line 41
  5. theorem OAI.LargePrimeGaps.extendLabels_injective line 44
  6. theorem OAI.LargePrimeGaps.extendLabels_range_ne line 53
  7. def OAI.LargePrimeGaps.extraPairLabels line 69
  8. def OAI.LargePrimeGaps.extraPairFamily line 74
  9. theorem OAI.LargePrimeGaps.castAdd_ne_natAdd line 79
  10. theorem OAI.LargePrimeGaps.natAdd_ne_castAdd line 86
  11. theorem OAI.LargePrimeGaps.extraPairFamily_matched line 89
  12. def OAI.LargePrimeGaps.extraPairProfile line 121
  13. theorem OAI.LargePrimeGaps.extraPairProfile_compact line 125
  14. theorem OAI.LargePrimeGaps.extraPairProfile_smooth line 131
  15. def OAI.LargePrimeGaps.extraPairKernel line 137
  16. theorem OAI.LargePrimeGaps.extraPairKernel_unmatched line 149
  17. theorem OAI.LargePrimeGaps.extraPairKernel_matched line 176
  18. def OAI.LargePrimeGaps.splitOffsets line 196
  19. theorem OAI.LargePrimeGaps.splitBox_mem line 199
  20. def OAI.LargePrimeGaps.splitBoxEquiv line 244
  21. theorem OAI.LargePrimeGaps.split_double_sum line 265
  22. theorem OAI.LargePrimeGaps.splitOffsets_eventually line 279
  23. def OAI.LargePrimeGaps.extraBoxLabels line 286
  24. theorem OAI.LargePrimeGaps.extraBoxLabels_surjective line 292
  25. def OAI.LargePrimeGaps.extraShifts line 303
  26. theorem OAI.LargePrimeGaps.extraBoxShifts_eq line 309
  27. theorem OAI.LargePrimeGaps.extra_pattern_sum_eq_box line 321
  28. theorem OAI.LargePrimeGaps.extra_square_pattern_sum line 341
  29. theorem OAI.LargePrimeGaps.extra_cross_pattern_sum line 379
  30. theorem OAI.LargePrimeGaps.extraBoxLabels_family line 402
  31. theorem OAI.LargePrimeGaps.extra_pattern_limit line 418
  32. def OAI.LargePrimeGaps.extraAverage line 440
  33. theorem OAI.LargePrimeGaps.extraAverage_finset_sum line 445
  34. theorem OAI.LargePrimeGaps.extra_divisor_product line 452
  35. theorem OAI.LargePrimeGaps.extra_block_expansion line 468
  36. theorem OAI.LargePrimeGaps.extra_labeled_limit line 501