OAI/Computability/VertexCover/PCP/AmplificationRound.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGames.Foundations.PCP.AmplificationRound.Label line 15
2. abbrev OAI.UniqueGames.Foundations.PCP.AmplificationRound.Addresses line 16
3. abbrev OAI.UniqueGames.Foundations.PCP.AmplificationRound.PoweredAlphabet line 17
4. instance OAI.UniqueGames.Foundations.PCP.AmplificationRound.(instance at line 20) line 20
5. instance OAI.UniqueGames.Foundations.PCP.AmplificationRound.(instance at line 21) line 21
6. abbrev OAI.UniqueGames.Foundations.PCP.AmplificationRound.PoweredDart line 26
7. instance OAI.UniqueGames.Foundations.PCP.AmplificationRound.(instance at line 30) line 30
8. def OAI.UniqueGames.Foundations.PCP.AmplificationRound.selectors line 32
9. def OAI.UniqueGames.Foundations.PCP.AmplificationRound.powered line 39
10. abbrev OAI.UniqueGames.Foundations.PCP.AmplificationRound.Vertex line 45
11. abbrev OAI.UniqueGames.Foundations.PCP.AmplificationRound.Dart line 50
12. instance OAI.UniqueGames.Foundations.PCP.AmplificationRound.(instance at line 53) line 53
13. instance OAI.UniqueGames.Foundations.PCP.AmplificationRound.(instance at line 62) line 62
14. instance OAI.UniqueGames.Foundations.PCP.AmplificationRound.(instance at line 65) line 65
15. def OAI.UniqueGames.Foundations.PCP.AmplificationRound.graph line 67
16. theorem OAI.UniqueGames.Foundations.PCP.AmplificationRound.powered_completeness line 72
17. theorem OAI.UniqueGames.Foundations.PCP.AmplificationRound.completeness line 85