OAI/Computability/VertexCover/Repetition/QuestionMarginal.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.Repetition.selectedTupleLikelihood line 52
2. theorem OAI.UniqueGames.Foundations.Repetition.selectedTupleLikelihood_nonnegative line 58
3. theorem OAI.UniqueGames.Foundations.Repetition.selectedTupleLikelihood_le_one line 66
4. theorem OAI.UniqueGames.Foundations.Repetition.selectedTupleLikelihood_mass line 74
5. def OAI.UniqueGames.Foundations.Repetition.selectedQuestionMarginal line 87
6. theorem OAI.UniqueGames.Foundations.Repetition.selectedQuestionMarginal_weight line 94
7. theorem OAI.UniqueGames.Foundations.Repetition.selectedQuestionMarginal_totalVariation_sq_sum_le_log line 112
8. theorem OAI.UniqueGames.Foundations.Repetition.unselectedQuestionMarginal_totalVariation_sq_sum_le_log line 130
9. theorem OAI.UniqueGames.Foundations.Repetition.unselectedQuestionMarginal_totalVariation_sum_le_sqrt line 152
10. theorem OAI.UniqueGames.Foundations.Repetition.unselectedQuestionMarginal_totalVariation_sum_le_sqrt_sub_card line 180