OAI/Combinatorics/SharpRamsey/Learning/PreparedDecoder.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpLogRamsey.GreedyPreparation.own_inter line 16
  2. lemma OAI.SharpLogRamsey.GreedyPreparation.own_public line 26
  3. def OAI.SharpLogRamsey.GreedyPreparation.sized line 30
  4. def OAI.SharpLogRamsey.GreedyPreparation.publicSize line 34
  5. lemma OAI.SharpLogRamsey.GreedyPreparation.sized_planes line 39
  6. lemma OAI.SharpLogRamsey.GreedyPreparation.publicSize_eq line 46
  7. def OAI.SharpLogRamsey.PreparedDecoder.counts line 65
  8. def OAI.SharpLogRamsey.PreparedDecoder.publicSample line 68
  9. def OAI.SharpLogRamsey.PreparedDecoder.publicScore line 71
  10. lemma OAI.SharpLogRamsey.PreparedDecoder.publicSample_eq line 77
  11. lemma OAI.SharpLogRamsey.PreparedDecoder.empty_counts line 94
  12. lemma OAI.SharpLogRamsey.PreparedDecoder.publicScore_eq line 105
  13. def OAI.SharpLogRamsey.PreparedDecoder.decode line 124
  14. theorem OAI.SharpLogRamsey.PreparedDecoder.decode_equals_source line 132