OAI/Computability/UniqueGames/Analysis/DyadicError.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniqueGamesTheorem.Appendix.DyadicError.pow_le_one_aux line 17
2. theorem OAI.UniqueGamesTheorem.Appendix.DyadicError.pow_antitone_aux line 25
3. theorem OAI.UniqueGamesTheorem.Appendix.DyadicError.half_power_le_quarter line 36
4. def OAI.UniqueGamesTheorem.Appendix.DyadicError.quarterSum line 49
5. theorem OAI.UniqueGamesTheorem.Appendix.DyadicError.quarterSum_nonneg line 51
6. theorem OAI.UniqueGamesTheorem.Appendix.DyadicError.quarterSum_residual line 55
7. theorem OAI.UniqueGamesTheorem.Appendix.DyadicError.quarterSum_le line 65
8. def OAI.UniqueGamesTheorem.Appendix.DyadicError.quarterError line 70
9. theorem OAI.UniqueGamesTheorem.Appendix.DyadicError.quarterError_add_one line 74
10. theorem OAI.UniqueGamesTheorem.Appendix.DyadicError.quarterError_le_seven_ninths line 112
11. def OAI.UniqueGamesTheorem.Appendix.DyadicError.dyadicError line 120
12. theorem OAI.UniqueGamesTheorem.Appendix.DyadicError.dyadicError_le_quarterError line 124
13. theorem OAI.UniqueGamesTheorem.Appendix.DyadicError.dyadicError_le_seven_ninths line 136
14. theorem OAI.UniqueGamesTheorem.Appendix.DyadicError.finite_dyadic_error_le_one line 141