OAI/Computability/VertexCover/PCP/ExpanderFamily.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGames.Foundations.PCP.ExpanderFamily.Port line 14
2. abbrev OAI.UniqueGames.Foundations.PCP.ExpanderFamily.CloudPort line 15
3. def OAI.UniqueGames.Foundations.PCP.ExpanderFamily.growth line 16
4. theorem OAI.UniqueGames.Foundations.PCP.ExpanderFamily.card_port line 18
5. theorem OAI.UniqueGames.Foundations.PCP.ExpanderFamily.card_cloudPort line 22
6. theorem OAI.UniqueGames.Foundations.PCP.ExpanderFamily.growth_gt_one line 28
7. theorem OAI.UniqueGames.Foundations.PCP.ExpanderFamily.port_degree_ge_eight line 31
8. def OAI.UniqueGames.Foundations.PCP.ExpanderFamily.baseVertexEquiv line 35
9. def OAI.UniqueGames.Foundations.PCP.ExpanderFamily.baseOnCloud line 38
10. theorem OAI.UniqueGames.Foundations.PCP.ExpanderFamily.baseOnCloud_certificate line 41
11. def OAI.UniqueGames.Foundations.PCP.ExpanderFamily.Vertex line 44
12. instance OAI.UniqueGames.Foundations.PCP.ExpanderFamily.vertexFintype line 48
13. instance OAI.UniqueGames.Foundations.PCP.ExpanderFamily.basePortNonempty line 56
14. instance OAI.UniqueGames.Foundations.PCP.ExpanderFamily.vertexNonempty line 59
15. def OAI.UniqueGames.Foundations.PCP.ExpanderFamily.graph line 67
16. theorem OAI.UniqueGames.Foundations.PCP.ExpanderFamily.graph_certificate line 71
17. def OAI.UniqueGames.Foundations.PCP.ExpanderFamily.family line 94
18. theorem OAI.UniqueGames.Foundations.PCP.ExpanderFamily.family_certificate line 96
19. theorem OAI.UniqueGames.Foundations.PCP.ExpanderFamily.card_vertex line 99
20. def OAI.UniqueGames.Foundations.PCP.ExpanderFamily.level line 106
21. def OAI.UniqueGames.Foundations.PCP.ExpanderFamily.size line 108
22. theorem OAI.UniqueGames.Foundations.PCP.ExpanderFamily.le_size line 110
23. theorem OAI.UniqueGames.Foundations.PCP.ExpanderFamily.size_le_mul line 112
24. theorem OAI.UniqueGames.Foundations.PCP.ExpanderFamily.padded_family_size line 126