OAI/NumberTheory/PowerFree/AdaptiveRanks.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuarticPowerFree.equationRank line 11
  2. theorem OAI.QuarticPowerFree.equationRank_mono line 14
  3. theorem OAI.QuarticPowerFree.equationRank_eq_iff_of_le line 20
  4. def OAI.QuarticPowerFree.adaptiveCode line 36
  5. def OAI.QuarticPowerFree.adaptiveStates line 41
  6. theorem OAI.QuarticPowerFree.adaptiveCode_lt line 47
  7. theorem OAI.QuarticPowerFree.adaptiveCode_mono_stable line 59
  8. theorem OAI.QuarticPowerFree.sum_subsets_erase line 86
  9. def OAI.QuarticPowerFree.subsetMean line 126
  10. theorem OAI.QuarticPowerFree.subset_incidence_card line 130
  11. theorem OAI.QuarticPowerFree.sum_subsets_members line 156
  12. theorem OAI.QuarticPowerFree.sum_subsets_complement line 165
  13. theorem OAI.QuarticPowerFree.subset_deletion_mean line 177
  14. theorem OAI.QuarticPowerFree.subset_marked_mean line 185
  15. def OAI.QuarticPowerFree.badFraction line 192
  16. theorem OAI.QuarticPowerFree.bad_indicator_le_rank_drop line 197
  17. theorem OAI.QuarticPowerFree.deleted_bad_sum_le line 210
  18. theorem OAI.QuarticPowerFree.deletion_one_step line 229
  19. theorem OAI.QuarticPowerFree.subsetMean_record_bounds line 272
  20. theorem OAI.QuarticPowerFree.deletion_average_bound line 288