OAI/Computability/VertexCover/PCP/PoweringTest.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.PCP.PoweringTest.baseGraph line 16
2. def OAI.UniqueGames.Foundations.PCP.PoweringTest.pathAccepts line 25
3. theorem OAI.UniqueGames.Foundations.PCP.PoweringTest.pathAccepts_eq_true_iff line 33
4. abbrev OAI.UniqueGames.Foundations.PCP.PoweringTest.Dart line 44
5. def OAI.UniqueGames.Foundations.PCP.PoweringTest.reverseDart line 46
6. theorem OAI.UniqueGames.Foundations.PCP.PoweringTest.reverseDart_involutive line 56
7. def OAI.UniqueGames.Foundations.PCP.PoweringTest.poweredGraph line 61
8. theorem OAI.UniqueGames.Foundations.PCP.PoweringTest.poweredGraph_tail_false line 73
9. theorem OAI.UniqueGames.Foundations.PCP.PoweringTest.poweredGraph_tail_true line 78
10. theorem OAI.UniqueGames.Foundations.PCP.PoweringTest.poweredGraph_edgeSatisfied line 83
11. theorem OAI.UniqueGames.Foundations.PCP.PoweringTest.rejection_mean_eq_path_mean line 92
12. theorem OAI.UniqueGames.Foundations.PCP.PoweringTest.pathAccepts_honest line 103
13. theorem OAI.UniqueGames.Foundations.PCP.PoweringTest.perfect_completeness line 117
14. theorem OAI.UniqueGames.Foundations.PCP.PoweringTest.preserves_satisfiability line 128
15. def OAI.UniqueGames.Foundations.PCP.PoweringTest.decodedBad line 140
16. theorem OAI.UniqueGames.Foundations.PCP.PoweringTest.decodedBad_eq_true_iff line 144
17. theorem OAI.UniqueGames.Foundations.PCP.PoweringTest.decodedBad_rot line 150
18. def OAI.UniqueGames.Foundations.PCP.PoweringTest.witness line 159
19. theorem OAI.UniqueGames.Foundations.PCP.PoweringTest.witness_bad line 171
20. theorem OAI.UniqueGames.Foundations.PCP.PoweringTest.witness_implies_path_rejection line 179
21. theorem OAI.UniqueGames.Foundations.PCP.PoweringTest.witness_implies_rejection line 206