OAI/Combinatorics/IndependentSets/Repetition/QuestionMarginal.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Repetition.selectedTupleLikelihood line 19
2. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedTupleLikelihood_nonnegative line 25
3. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedTupleLikelihood_le_one line 33
4. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedTupleLikelihood_mass line 41
5. def OAI.IndependentSetsGames.Foundations.Repetition.selectedQuestionMarginal line 54
6. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedQuestionMarginal_weight line 61
7. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedQuestionMarginal_totalVariation_sq_sum_le_log line 79
8. theorem OAI.IndependentSetsGames.Foundations.Repetition.unselectedQuestionMarginal_totalVariation_sq_sum_le_log line 97
9. theorem OAI.IndependentSetsGames.Foundations.Repetition.unselectedQuestionMarginal_totalVariation_sum_le_sqrt line 119
10. theorem OAI.IndependentSetsGames.Foundations.Repetition.unselectedQuestionMarginal_totalVariation_sum_le_sqrt_sub_card line 147