OAI/Computability/VertexCover/PCP/PoweringReturn.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.PCP.PoweringReturn.portConsEquiv line 16
2. theorem OAI.UniqueGames.Foundations.PCP.PoweringReturn.mean_word_cons_head line 29
3. theorem OAI.UniqueGames.Foundations.PCP.PoweringReturn.mean_word_cons_tail line 37
4. theorem OAI.UniqueGames.Foundations.PCP.PoweringReturn.iterateOperator_succ_right line 45
5. theorem OAI.UniqueGames.Foundations.PCP.PoweringReturn.mean_wordEnd line 52
6. theorem OAI.UniqueGames.Foundations.PCP.PoweringReturn.mean_pivot_endpoints line 73
7. theorem OAI.UniqueGames.Foundations.PCP.PoweringReturn.mean_edge_endpoints line 115
8. theorem OAI.UniqueGames.Foundations.PCP.PoweringReturn.bit_bool line 139
9. theorem OAI.UniqueGames.Foundations.PCP.PoweringReturn.mean_edge_bit line 142
10. theorem OAI.UniqueGames.Foundations.PCP.PoweringReturn.mean_marked_bit line 146
11. theorem OAI.UniqueGames.Foundations.PCP.PoweringReturn.edgeAt_zero line 156
12. theorem OAI.UniqueGames.Foundations.PCP.PoweringReturn.word_first_hit_mean line 160
13. theorem OAI.UniqueGames.Foundations.PCP.PoweringReturn.word_hit_mean line 171
14. theorem OAI.UniqueGames.Foundations.PCP.PoweringReturn.word_pair_hit_mean line 198
15. theorem OAI.UniqueGames.Foundations.PCP.PoweringReturn.hit_mean line 256
16. theorem OAI.UniqueGames.Foundations.PCP.PoweringReturn.pair_hit_mean line 272
17. theorem OAI.UniqueGames.Foundations.PCP.PoweringReturn.pair_event_mean line 293