OAI/Combinatorics/RamseyFive/Decoding/Best.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpRamseyFive.GreedyTraining.maximizers_nonempty line 12
  2. def OAI.SharpRamseyFive.GreedyTraining.best line 18
  3. lemma OAI.SharpRamseyFive.GreedyTraining.best_spec line 23
  4. def OAI.SharpRamseyFive.GreedyTraining.remaining line 28
  5. def OAI.SharpRamseyFive.GreedyTraining.chosen line 33
  6. def OAI.SharpRamseyFive.GreedyTraining.cell line 36
  7. lemma OAI.SharpRamseyFive.GreedyTraining.chosen_mem line 42
  8. lemma OAI.SharpRamseyFive.GreedyTraining.maximal_cell line 45
  9. lemma OAI.SharpRamseyFive.GreedyTraining.remaining_succ_subset line 49
  10. lemma OAI.SharpRamseyFive.GreedyTraining.remaining_antitone line 52
  11. lemma OAI.SharpRamseyFive.GreedyTraining.remaining_subset line 55
  12. lemma OAI.SharpRamseyFive.GreedyTraining.cell_subset line 58
  13. lemma OAI.SharpRamseyFive.GreedyTraining.cell_card_antitone line 61
  14. lemma OAI.SharpRamseyFive.GreedyTraining.cell_card_add_remaining line 69
  15. lemma OAI.SharpRamseyFive.GreedyTraining.sum_card_add_remaining line 74
  16. lemma OAI.SharpRamseyFive.GreedyTraining.cell_disjoint_of_lt line 83
  17. def OAI.SharpRamseyFive.GreedyTraining.Stop line 92
  18. lemma OAI.SharpRamseyFive.GreedyTraining.exists_stop line 96
  19. def OAI.SharpRamseyFive.GreedyTraining.stopIndex line 112
  20. lemma OAI.SharpRamseyFive.GreedyTraining.stopIndex_stops line 115
  21. lemma OAI.SharpRamseyFive.GreedyTraining.before_stop line 118
  22. lemma OAI.SharpRamseyFive.GreedyTraining.stopIndex_le_card line 126
  23. lemma OAI.SharpRamseyFive.GreedyTraining.list_length_bound line 131
  24. def OAI.SharpRamseyFive.GreedyTraining.retained line 141
  25. lemma OAI.SharpRamseyFive.GreedyTraining.retained_subset line 146
  26. lemma OAI.SharpRamseyFive.GreedyTraining.retained_half line 153
  27. lemma OAI.SharpRamseyFive.GreedyTraining.residual_cap line 165
  28. lemma OAI.SharpRamseyFive.GreedyTraining.remaining_eq_sdiff_union line 173
  29. lemma OAI.SharpRamseyFive.GreedyTraining.prefix_length_bound line 199
  30. lemma OAI.SharpRamseyFive.GreedyTraining.tail_cap line 207
  31. def OAI.SharpRamseyFive.GreedyTraining.headIndex line 213
  32. lemma OAI.SharpRamseyFive.GreedyTraining.headIndex_le line 216
  33. lemma OAI.SharpRamseyFive.GreedyTraining.before_head line 219
  34. lemma OAI.SharpRamseyFive.GreedyTraining.head_length_bound line 224
  35. lemma OAI.SharpRamseyFive.GreedyTraining.head_tail_cap line 227
  36. lemma OAI.SharpRamseyFive.GreedyTraining.captured_eq_biUnion_cells line 235
  37. lemma OAI.SharpRamseyFive.GreedyTraining.cell_earliest line 248
  38. def OAI.SharpRamseyFive.GreedyTraining.firstAt line 256
  39. lemma OAI.SharpRamseyFive.GreedyTraining.firstAt_le line 259
  40. lemma OAI.SharpRamseyFive.GreedyTraining.firstAt_mem line 262
  41. lemma OAI.SharpRamseyFive.GreedyTraining.firstAt_eq line 268
  42. def OAI.SharpRamseyFive.GreedyTraining.ownCell line 278
  43. lemma OAI.SharpRamseyFive.GreedyTraining.ownCell_eq line 281