OAI/Combinatorics/IndependentSets/Expansion/Overlay.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.Overlay.originalPortGraph line 15
2. def OAI.IndependentSetsGames.Foundations.PCP.Overlay.rotate line 19
3. theorem OAI.IndependentSetsGames.Foundations.PCP.Overlay.rotate_involutive line 24
4. def OAI.IndependentSetsGames.Foundations.PCP.Overlay.portGraph line 33
5. theorem OAI.IndependentSetsGames.Foundations.PCP.Overlay.portGraph_rot_inl line 41
6. theorem OAI.IndependentSetsGames.Foundations.PCP.Overlay.portGraph_rot_inr line 46
7. def OAI.IndependentSetsGames.Foundations.PCP.Overlay.constraintGraph line 51
8. theorem OAI.IndependentSetsGames.Foundations.PCP.Overlay.constraintGraph_tail line 65
9. theorem OAI.IndependentSetsGames.Foundations.PCP.Overlay.constraintGraph_portGraph line 68
10. theorem OAI.IndependentSetsGames.Foundations.PCP.Overlay.edgeSatisfied_inl line 72
11. theorem OAI.IndependentSetsGames.Foundations.PCP.Overlay.edgeSatisfied_inr line 82
12. theorem OAI.IndependentSetsGames.Foundations.PCP.Overlay.complete line 86
13. theorem OAI.IndependentSetsGames.Foundations.PCP.Overlay.satisfiable_iff line 96
14. theorem OAI.IndependentSetsGames.Foundations.PCP.Overlay.rejectionCount_eq line 108
15. theorem OAI.IndependentSetsGames.Foundations.PCP.Overlay.card_ports line 117
16. theorem OAI.IndependentSetsGames.Foundations.PCP.Overlay.card_darts line 120
17. theorem OAI.IndependentSetsGames.Foundations.PCP.Overlay.operator_mix line 129
18. theorem OAI.IndependentSetsGames.Foundations.PCP.Overlay.energy_convex_mix line 148
19. theorem OAI.IndependentSetsGames.Foundations.PCP.Overlay.energy_bound line 163
20. theorem OAI.IndependentSetsGames.Foundations.PCP.Overlay.energy_bound_three_quarters line 198
21. theorem OAI.IndependentSetsGames.Foundations.PCP.Overlay.spectralCertificate_seven_eighths line 217
22. theorem OAI.IndependentSetsGames.Foundations.PCP.Overlay.constraintGraph_spectralCertificate line 230