OAI/Combinatorics/IndependentSets/Repetition/ProfileBounds.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.IndependentSetsGames.Foundations.Repetition.firstMarginal_totalVariation_le line 14
2. def OAI.IndependentSetsGames.Foundations.Repetition.leftCommonMarginal line 23
3. def OAI.IndependentSetsGames.Foundations.Repetition.leftCommonProfile line 26
4. def OAI.IndependentSetsGames.Foundations.Repetition.swapSeedLeft line 29
5. theorem OAI.IndependentSetsGames.Foundations.Repetition.leftCommonMarginal_isProbability line 35
6. theorem OAI.IndependentSetsGames.Foundations.Repetition.leftCommonProfile_isProbability line 40
7. theorem OAI.IndependentSetsGames.Foundations.Repetition.leftCommonProfile_error line 45
8. def OAI.IndependentSetsGames.Foundations.Repetition.swapQuestionEndpoints line 82
9. def OAI.IndependentSetsGames.Foundations.Repetition.rightCommonMarginal line 88
10. def OAI.IndependentSetsGames.Foundations.Repetition.rightCommonProfile line 91
11. theorem OAI.IndependentSetsGames.Foundations.Repetition.rightCommonProfile_isProbability line 94
12. theorem OAI.IndependentSetsGames.Foundations.Repetition.swap_question_pushforward_snd line 100
13. theorem OAI.IndependentSetsGames.Foundations.Repetition.leftRevealModel_swap line 106
14. theorem OAI.IndependentSetsGames.Foundations.Repetition.rightCommonProfile_error line 116