OAI/Combinatorics/RamseyFive/Decoding/MetadataCodec.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.Metadata.projective_card_le_vectors line 18
2. def OAI.SharpRamseyFive.Metadata.encodeLists line 27
3. def OAI.SharpRamseyFive.Metadata.decodeH line 40
4. def OAI.SharpRamseyFive.Metadata.decodeP line 42
5. def OAI.SharpRamseyFive.Metadata.decodeOwn line 44
6. def OAI.SharpRamseyFive.Metadata.decodeOwnCount line 47
7. lemma OAI.SharpRamseyFive.Metadata.decodeH_encode line 56
8. lemma OAI.SharpRamseyFive.Metadata.decodeP_encode line 62
9. lemma OAI.SharpRamseyFive.Metadata.decodeOwn_encode line 69
10. theorem OAI.SharpRamseyFive.Metadata.decodeOwnCount_encode line 76
11. def OAI.SharpRamseyFive.Metadata.decodeBaseScore line 87
12. lemma OAI.SharpRamseyFive.Metadata.decodeBaseScore_encode line 90
13. lemma OAI.SharpRamseyFive.Metadata.vector_card_le_exp line 107
14. def OAI.SharpRamseyFive.Metadata.encodeTraining line 117
15. def OAI.SharpRamseyFive.Metadata.messageOwn line 124
16. def OAI.SharpRamseyFive.Metadata.messageBase line 126
17. theorem OAI.SharpRamseyFive.Metadata.training_message line 129