OAI/Computability/VertexCover/PCP/PoweringTableSemantics.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGames.Foundations.PCP.PoweringTableSemantics.RawLabeling line 13
2. abbrev OAI.UniqueGames.Foundations.PCP.PoweringTableSemantics.EncodedLabeling line 16
3. def OAI.UniqueGames.Foundations.PCP.PoweringTableSemantics.encodeLabeling line 19
4. def OAI.UniqueGames.Foundations.PCP.PoweringTableSemantics.decodeLabeling line 23
5. theorem OAI.UniqueGames.Foundations.PCP.PoweringTableSemantics.decodeLabeling_encodeLabeling line 27
6. theorem OAI.UniqueGames.Foundations.PCP.PoweringTableSemantics.encodeLabeling_decodeLabeling line 33
7. theorem OAI.UniqueGames.Foundations.PCP.PoweringTableSemantics.edgeSatisfied_encoded line 39
8. theorem OAI.UniqueGames.Foundations.PCP.PoweringTableSemantics.edgeSatisfied_decoded line 51
9. theorem OAI.UniqueGames.Foundations.PCP.PoweringTableSemantics.edgeSatisfied_eq_path line 65
10. theorem OAI.UniqueGames.Foundations.PCP.PoweringTableSemantics.rejectionCount_encoded line 80
11. theorem OAI.UniqueGames.Foundations.PCP.PoweringTableSemantics.rejectionCount_decoded line 90
12. theorem OAI.UniqueGames.Foundations.PCP.PoweringTableSemantics.card_darts_eq_table line 101
13. theorem OAI.UniqueGames.Foundations.PCP.PoweringTableSemantics.satisfiable_iff line 108
14. theorem OAI.UniqueGames.Foundations.PCP.PoweringTableSemantics.preserves_satisfiability line 125
15. theorem OAI.UniqueGames.Foundations.PCP.PoweringTableSemantics.path_rejection_mean_eq_table_fraction line 133
16. theorem OAI.UniqueGames.Foundations.PCP.PoweringTableSemantics.uniform_count_gap_iff line 148
17. theorem OAI.UniqueGames.Foundations.PCP.PoweringTableSemantics.uniform_count_gap line 171