OAI/Computability/VertexCover/PCP/Overlay.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.PCP.Overlay.originalPortGraph line 17
2. def OAI.UniqueGames.Foundations.PCP.Overlay.rotate line 21
3. theorem OAI.UniqueGames.Foundations.PCP.Overlay.rotate_involutive line 26
4. def OAI.UniqueGames.Foundations.PCP.Overlay.portGraph line 35
5. theorem OAI.UniqueGames.Foundations.PCP.Overlay.portGraph_rot_inl line 43
6. theorem OAI.UniqueGames.Foundations.PCP.Overlay.portGraph_rot_inr line 48
7. def OAI.UniqueGames.Foundations.PCP.Overlay.constraintGraph line 53
8. theorem OAI.UniqueGames.Foundations.PCP.Overlay.constraintGraph_tail line 67
9. theorem OAI.UniqueGames.Foundations.PCP.Overlay.constraintGraph_portGraph line 70
10. theorem OAI.UniqueGames.Foundations.PCP.Overlay.edgeSatisfied_inl line 74
11. theorem OAI.UniqueGames.Foundations.PCP.Overlay.edgeSatisfied_inr line 84
12. theorem OAI.UniqueGames.Foundations.PCP.Overlay.complete line 88
13. theorem OAI.UniqueGames.Foundations.PCP.Overlay.satisfiable_iff line 98
14. theorem OAI.UniqueGames.Foundations.PCP.Overlay.rejectionCount_eq line 110
15. theorem OAI.UniqueGames.Foundations.PCP.Overlay.card_ports line 119
16. theorem OAI.UniqueGames.Foundations.PCP.Overlay.card_darts line 122
17. theorem OAI.UniqueGames.Foundations.PCP.Overlay.operator_mix line 131
18. theorem OAI.UniqueGames.Foundations.PCP.Overlay.energy_convex_mix line 150
19. theorem OAI.UniqueGames.Foundations.PCP.Overlay.energy_bound line 165
20. theorem OAI.UniqueGames.Foundations.PCP.Overlay.energy_bound_three_quarters line 200
21. theorem OAI.UniqueGames.Foundations.PCP.Overlay.spectralCertificate_seven_eighths line 219
22. theorem OAI.UniqueGames.Foundations.PCP.Overlay.constraintGraph_spectralCertificate line 232