OAI/Computability/VertexCover/PCP/PoweringLabels.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGames.Foundations.PCP.PoweringLabels.PortWords line 15
2. instance OAI.UniqueGames.Foundations.PCP.PoweringLabels.finitePortWords line 17
3. def OAI.UniqueGames.Foundations.PCP.PoweringLabels.Ball line 21
4. def OAI.UniqueGames.Foundations.PCP.PoweringLabels.wordToBall line 24
5. theorem OAI.UniqueGames.Foundations.PCP.PoweringLabels.wordToBall_surjective line 27
6. instance OAI.UniqueGames.Foundations.PCP.PoweringLabels.finiteBall line 34
7. theorem OAI.UniqueGames.Foundations.PCP.PoweringLabels.card_portWords line 38
8. theorem OAI.UniqueGames.Foundations.PCP.PoweringLabels.card_ball_le line 42
9. structure OAI.UniqueGames.Foundations.PCP.PoweringLabels.AddressSelector line 49
10. def OAI.UniqueGames.Foundations.PCP.PoweringLabels.classicalSelector line 53
11. def OAI.UniqueGames.Foundations.PCP.PoweringLabels.scanWitness line 58
12. def OAI.UniqueGames.Foundations.PCP.PoweringLabels.listSelector line 69
13. abbrev OAI.UniqueGames.Foundations.PCP.PoweringLabels.PaddedLabel line 80
14. def OAI.UniqueGames.Foundations.PCP.PoweringLabels.encode line 82
15. def OAI.UniqueGames.Foundations.PCP.PoweringLabels.decode line 85
16. theorem OAI.UniqueGames.Foundations.PCP.PoweringLabels.decode_encode line 88
17. theorem OAI.UniqueGames.Foundations.PCP.PoweringLabels.decode_surjective line 95
18. theorem OAI.UniqueGames.Foundations.PCP.PoweringLabels.encode_injective line 99
19. theorem OAI.UniqueGames.Foundations.PCP.PoweringLabels.decoded_word_collision line 106
20. theorem OAI.UniqueGames.Foundations.PCP.PoweringLabels.card_paddedLabel line 112