OAI/NumberTheory/PowerFree/PrimeBlocks.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.product_distinct_prime_divisors_le line 12
  2. theorem OAI.QuarticPowerFree.card_large_prime_divisors_le line 29
  3. theorem OAI.QuarticPowerFree.card_large_prime_divisors_le_floor line 46
  4. def OAI.QuarticPowerFree.cellKernel line 55
  5. theorem OAI.QuarticPowerFree.cellKernel_mono line 59
  6. theorem OAI.QuarticPowerFree.adaptiveStates_length line 66
  7. theorem OAI.QuarticPowerFree.list_minor_product_bound line 73
  8. theorem OAI.QuarticPowerFree.adaptive_deletion_bound line 89
  9. def OAI.QuarticPowerFree.BlockSample line 135
  10. instance OAI.QuarticPowerFree.(instance at line 138) line 138
  11. def OAI.QuarticPowerFree.blockWeight line 141
  12. def OAI.QuarticPowerFree.blockSet line 145
  13. theorem OAI.QuarticPowerFree.blockSet_spec line 148
  14. theorem OAI.QuarticPowerFree.blockWeight_nonneg line 152
  15. theorem OAI.QuarticPowerFree.blockWeight_sum line 157
  16. theorem OAI.QuarticPowerFree.blockWeight_bad_average line 174
  17. theorem OAI.QuarticPowerFree.independent_average_le line 198
  18. theorem OAI.QuarticPowerFree.exists_many_regular line 248
  19. theorem OAI.QuarticPowerFree.bad_blocks_indicator_le line 286