OAI/Combinatorics/RamseyFive/Decoding/Training.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.GreedyTraining.Captured line 10
  2. def OAI.SharpRamseyFive.GreedyTraining.peelSet line 14
  3. def OAI.SharpRamseyFive.GreedyTraining.peelLength line 18
  4. lemma OAI.SharpRamseyFive.GreedyTraining.peel_subset line 22
  5. lemma OAI.SharpRamseyFive.GreedyTraining.peel_half line 30
  6. lemma OAI.SharpRamseyFive.GreedyTraining.peel_length_bound line 38
  7. lemma OAI.SharpRamseyFive.GreedyTraining.peel_alternative line 46
  8. lemma OAI.SharpRamseyFive.GreedyTraining.cell_subset_captured line 59
  9. lemma OAI.SharpRamseyFive.GreedyTraining.ownCell_zero line 66
  10. lemma OAI.SharpRamseyFive.GreedyTraining.peel_own_subset line 70
  11. lemma OAI.SharpRamseyFive.GreedyTraining.two_peels_quarter line 83
  12. lemma OAI.SharpRamseyFive.GreedyTraining.peel_length_real line 91
  13. lemma OAI.SharpRamseyFive.GreedyTraining.peel_residual_real line 100
  14. def OAI.SharpRamseyFive.GreedyTraining.clippedPart line 110
  15. def OAI.SharpRamseyFive.GreedyTraining.queryPart line 115
  16. lemma OAI.SharpRamseyFive.GreedyTraining.clippedPart_subset line 119
  17. lemma OAI.SharpRamseyFive.GreedyTraining.clippedPart_disjoint line 126
  18. lemma OAI.SharpRamseyFive.GreedyTraining.clippedPart_query line 142
  19. def OAI.SharpRamseyFive.TrainingCells.family line 156
  20. lemma OAI.SharpRamseyFive.TrainingCells.sum_card_le line 161
  21. lemma OAI.SharpRamseyFive.TrainingCells.inter_disjoint line 170
  22. lemma OAI.SharpRamseyFive.TrainingCells.family_mass line 179
  23. lemma OAI.SharpRamseyFive.TrainingCells.family_subsets line 191
  24. lemma OAI.SharpRamseyFive.TrainingCells.small_union line 198