OAI/NumberTheory/PrimeGaps/MarkedMoments.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargePrimeGaps.orderedWeight_marked_limit line 27
  2. theorem OAI.LargePrimeGaps.deleteCoordinate_smooth line 65
  3. theorem OAI.LargePrimeGaps.deleteCoordinate_tsupport_subset line 94
  4. theorem OAI.LargePrimeGaps.deleteCoordinate_compact line 109
  5. theorem OAI.LargePrimeGaps.deleteCoordinate_interior_support line 114
  6. def OAI.LargePrimeGaps.fixLastPerm line 127
  7. theorem OAI.LargePrimeGaps.fixLastPerm_castSucc line 130
  8. theorem OAI.LargePrimeGaps.fixLastPerm_last line 136
  9. theorem OAI.LargePrimeGaps.deleteCoordinate_symmetric line 142
  10. theorem OAI.LargePrimeGaps.pi_restrict_Ici line 153
  11. theorem OAI.LargePrimeGaps.integral_Ici_snoc line 160
  12. theorem OAI.LargePrimeGaps.cumulativeProfile_delete_tail line 180
  13. def OAI.LargePrimeGaps.deletedFamily line 195
  14. theorem OAI.LargePrimeGaps.AdmissibleFamily.all_properties line 198
  15. theorem OAI.LargePrimeGaps.deletedFamily_admissible line 209
  16. theorem OAI.LargePrimeGaps.cumulativeProfile_deletedFamily line 228
  17. theorem OAI.LargePrimeGaps.divisorSum_add line 243
  18. theorem OAI.LargePrimeGaps.divisorSum_internal_family_delete line 247
  19. theorem OAI.LargePrimeGaps.orderedDetector_eq_detector line 261
  20. theorem OAI.LargePrimeGaps.unorderedWeight_external_marked_limit line 273
  21. def OAI.LargePrimeGaps.setDivisor line 283
  22. theorem OAI.LargePrimeGaps.subsetEnumeration_range line 287
  23. theorem OAI.LargePrimeGaps.setDivisor_eq_enumeration line 293
  24. theorem OAI.LargePrimeGaps.snoc_subsetEnumeration_injective line 306
  25. theorem OAI.LargePrimeGaps.snoc_subsetEnumeration_range line 331
  26. theorem OAI.LargePrimeGaps.setDivisor_insert_eq_snoc line 350
  27. def OAI.LargePrimeGaps.finiteSubsetWeight line 363
  28. theorem OAI.LargePrimeGaps.finiteSubsetWeight_prime_delete line 367
  29. theorem OAI.LargePrimeGaps.setDivisor_fixed_card line 388
  30. theorem OAI.LargePrimeGaps.setDivisor_level_sum line 395
  31. theorem OAI.LargePrimeGaps.cumulativeProfile_zero line 407
  32. theorem OAI.LargePrimeGaps.divisorSum_zero line 412
  33. theorem OAI.LargePrimeGaps.unorderedBlock_zero line 416
  34. theorem OAI.LargePrimeGaps.finiteSubsetWeight_eq_unordered_levels line 420
  35. theorem OAI.LargePrimeGaps.unorderedWeight_eq_finiteSubsetWeight line 434
  36. def OAI.LargePrimeGaps.restrictedUnorderedBlock line 441
  37. def OAI.LargePrimeGaps.restrictedBlock line 446
  38. theorem OAI.LargePrimeGaps.enumeratePerm_subset_iff line 451
  39. theorem OAI.LargePrimeGaps.restrictedBlock_eq_unordered line 464
  40. theorem OAI.LargePrimeGaps.setDivisor_subset_level_sum line 494
  41. theorem OAI.LargePrimeGaps.restrictedUnorderedBlock_zero line 507