OAI/NumberTheory/PrimeGaps/RestrictedWeights.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LargePrimeGaps.finiteSubsetWeight_eq_restricted_levels line 27
2. def OAI.LargePrimeGaps.restrictedWeight line 46
3. theorem OAI.LargePrimeGaps.restrictedWeight_eq_finiteSubsetWeight line 51
4. theorem OAI.LargePrimeGaps.unorderedWeight_prime_delete line 63
5. theorem OAI.LargePrimeGaps.coincident_double_sum line 72
6. theorem OAI.LargePrimeGaps.patternTupleEquiv_avoid line 95
7. theorem OAI.LargePrimeGaps.pattern_restricted_marked_sum_eq_box line 115
8. theorem OAI.LargePrimeGaps.restricted_marked_pattern_limit line 136
9. def OAI.LargePrimeGaps.internalMarked line 159
10. theorem OAI.LargePrimeGaps.restrictedBlock_marked_expansion line 162
11. theorem OAI.LargePrimeGaps.restrictedBlock_marked_limit line 185
12. theorem OAI.LargePrimeGaps.restrictedBlock_mul line 227
13. theorem OAI.LargePrimeGaps.restrictedBlock_congr_orthant line 251
14. theorem OAI.LargePrimeGaps.restrictedBlock_cumulative_mul line 259
15. theorem OAI.LargePrimeGaps.internalMarked_congr line 277
16. theorem OAI.LargePrimeGaps.internalMarked_finset_sum line 284
17. theorem OAI.LargePrimeGaps.restricted_cumulative_pair_limit line 291
18. theorem OAI.LargePrimeGaps.restricted_cumulative_square_limit line 336
19. theorem OAI.LargePrimeGaps.restricted_cumulative_cross_limit line 348
20. theorem OAI.LargePrimeGaps.restrictedWeight_marked_limit line 362
21. theorem OAI.LargePrimeGaps.detector_I_eq line 399
22. theorem OAI.LargePrimeGaps.unorderedWeight_internal_delete_average line 413
23. theorem OAI.LargePrimeGaps.unorderedWeight_internal_marked_limit line 431
24. theorem OAI.LargePrimeGaps.cumulative_tensor_permuted_kernel_invariant line 444
25. theorem OAI.LargePrimeGaps.l2Mass_tensor line 485
26. def OAI.LargePrimeGaps.extendPerm line 494
27. theorem OAI.LargePrimeGaps.extendPerm_left line 497
28. theorem OAI.LargePrimeGaps.extendPerm_right line 501