OAI/NumberTheory/PrimeGaps/PatternMoments.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargePrimeGaps.box_series_scaled_tendsto line 27
  2. theorem OAI.LargePrimeGaps.distinctBox_init line 61
  3. theorem OAI.LargePrimeGaps.patternBoxShifts_ne_mark line 68
  4. theorem OAI.LargePrimeGaps.marked_patternBoxShifts_image line 82
  5. theorem OAI.LargePrimeGaps.marked_box_pattern_limit line 101
  6. def OAI.LargePrimeGaps.patternLabels line 174
  7. theorem OAI.LargePrimeGaps.patternLabels_surjective line 178
  8. theorem OAI.LargePrimeGaps.patternTupleEquiv_labels line 185
  9. theorem OAI.LargePrimeGaps.pattern_sum_average_eq_box line 193
  10. theorem OAI.LargePrimeGaps.unmarked_pattern_limit line 206
  11. theorem OAI.LargePrimeGaps.unmarked_labeled_expansion_limit line 231
  12. def OAI.LargePrimeGaps.permutedLabels line 267
  13. theorem OAI.LargePrimeGaps.permutedLabels_fiber_sum line 269
  14. theorem OAI.LargePrimeGaps.permutedLabels_fiber_card line 276
  15. theorem OAI.LargePrimeGaps.permutedLabels_classical_fiber line 280
  16. theorem OAI.LargePrimeGaps.permutedLabels_kernel line 287
  17. def OAI.LargePrimeGaps.permutedRay line 296
  18. theorem OAI.LargePrimeGaps.permutedRay_frequency line 299
  19. theorem OAI.LargePrimeGaps.permutedRay_positive line 308
  20. theorem OAI.LargePrimeGaps.rayVector_permuted line 315
  21. theorem OAI.LargePrimeGaps.permuted_kernelConstant line 330
  22. theorem OAI.LargePrimeGaps.cumulative_tensor_permuted_kernel line 344
  23. def OAI.LargePrimeGaps.functionPerm line 385
  24. theorem OAI.LargePrimeGaps.divisorCoefficient_perm line 391
  25. theorem OAI.LargePrimeGaps.divisorSum_perm line 400
  26. theorem OAI.LargePrimeGaps.injective_same_range_perm line 413
  27. def OAI.LargePrimeGaps.weightedBlock line 428
  28. def OAI.LargePrimeGaps.tensorCoefficient line 432
  29. theorem OAI.LargePrimeGaps.append_ker_left line 436
  30. theorem OAI.LargePrimeGaps.append_ker_right line 444
  31. theorem OAI.LargePrimeGaps.weightedBlock_mul line 452
  32. theorem OAI.LargePrimeGaps.average_weightedBlock line 472