OAI/Combinatorics/SharpRamsey/Learning/TestRowScore.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SharpLogRamsey.PreparedRow.Schedule line 14
  2. def OAI.SharpLogRamsey.PreparedRow.extend line 16
  3. def OAI.SharpLogRamsey.PreparedRow.sample line 19
  4. def OAI.SharpLogRamsey.PreparedRow.empty line 22
  5. def OAI.SharpLogRamsey.PreparedRow.emptySet line 25
  6. def OAI.SharpLogRamsey.PreparedRow.score line 28
  7. lemma OAI.SharpLogRamsey.PreparedRow.unsampled line 33
  8. lemma OAI.SharpLogRamsey.PreparedRow.sample_subset line 42
  9. lemma OAI.SharpLogRamsey.PreparedRow.score_eq line 45
  10. lemma OAI.SharpLogRamsey.PreparedRow.score_partition line 55
  11. lemma OAI.SharpLogRamsey.PreparedRow.empty_iff line 66
  12. lemma OAI.SharpLogRamsey.PreparedRow.score_exceptional_term line 74
  13. lemma OAI.SharpLogRamsey.PreparedRow.own_outside_union line 88
  14. theorem OAI.SharpLogRamsey.PreparedRow.exceptional_error line 98