OAI/Combinatorics/IndependentSets/Expansion/ExpanderFamily.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.Port line 11
2. abbrev OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.CloudPort line 12
3. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.growth line 13
4. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.card_port line 15
5. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.card_cloudPort line 19
6. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.growth_gt_one line 25
7. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.port_degree_ge_eight line 28
8. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.baseVertexEquiv line 32
9. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.baseOnCloud line 35
10. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.baseOnCloud_certificate line 38
11. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.Vertex line 41
12. instance OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.vertexFintype line 45
13. instance OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.basePortNonempty line 53
14. instance OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.vertexNonempty line 56
15. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.graph line 64
16. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.graph_certificate line 68
17. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.family line 91
18. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.family_certificate line 93
19. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.card_vertex line 96
20. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.level line 103
21. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.size line 105
22. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.le_size line 107
23. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.size_le_mul line 109
24. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderFamily.padded_family_size line 123
25. def OAI.IndependentSetsGames.Foundations.PCP.CloudPadding.paddedSize line 137
26. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudPadding.paddedSize_zero line 139
27. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudPadding.paddedSize_of_pos line 141
28. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudPadding.le_paddedSize line 145
29. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudPadding.paddedSize_le_mul line 152
30. def OAI.IndependentSetsGames.Foundations.PCP.CloudPadding.paddedCloudEquiv line 159
31. def OAI.IndependentSetsGames.Foundations.PCP.CloudPadding.dartCloudEquiv line 182