OAI/Computability/VertexCover/PCP/PoweringLazy.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.PCP.PoweringWalks.lazyRotate line 13
2. theorem OAI.UniqueGames.Foundations.PCP.PoweringWalks.lazyRotate_involutive line 17
3. def OAI.UniqueGames.Foundations.PCP.PoweringWalks.lazyGraph line 25
4. theorem OAI.UniqueGames.Foundations.PCP.PoweringWalks.lazyGraph_rot_false line 33
5. theorem OAI.UniqueGames.Foundations.PCP.PoweringWalks.lazyGraph_rot_true line 36
6. theorem OAI.UniqueGames.Foundations.PCP.PoweringLazy.operator_binomialMean line 47
7. theorem OAI.UniqueGames.Foundations.PCP.PoweringLazy.averagingOperator_lazy line 55
8. theorem OAI.UniqueGames.Foundations.PCP.PoweringLazy.iterate_lazy_eq_binomialMean line 67
9. theorem OAI.UniqueGames.Foundations.PCP.PoweringLazy.iterate_mem_Icc line 81
10. theorem OAI.UniqueGames.Foundations.PCP.PoweringLazy.lazy_endpoint_modal_transfer line 96