OAI/Combinatorics/IndependentSets/Repetition/SharedSampling.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Repetition.TraceSeed line 15
2. instance OAI.IndependentSetsGames.Foundations.Repetition.traceSeedFintype line 19
3. instance OAI.IndependentSetsGames.Foundations.Repetition.traceSeedUniqueZero line 24
4. def OAI.IndependentSetsGames.Foundations.Repetition.traceList line 27
5. def OAI.IndependentSetsGames.Foundations.Repetition.traceSeedLaw line 31
6. theorem OAI.IndependentSetsGames.Foundations.Repetition.traceSeedLaw_expectation line 37
7. def OAI.IndependentSetsGames.Foundations.Repetition.sharedOutputLaw line 54
8. theorem OAI.IndependentSetsGames.Foundations.Repetition.sharedOutputLaw_weight line 62
9. def OAI.IndependentSetsGames.Foundations.Repetition.samplerLocal line 80
10. def OAI.IndependentSetsGames.Foundations.Repetition.samplerOutputLaw line 86
11. theorem OAI.IndependentSetsGames.Foundations.Repetition.probability_weight_le_one line 93
12. theorem OAI.IndependentSetsGames.Foundations.Repetition.samplerOutputLaw_diagonal line 99
13. theorem OAI.IndependentSetsGames.Foundations.Repetition.samplerOutputLaw_uniform_diagonal line 130
14. theorem OAI.IndependentSetsGames.Foundations.Repetition.samplerOutputLaw_totalVariation line 150
15. theorem OAI.IndependentSetsGames.Foundations.Repetition.samplerOutputLaw_arbitrarily_close line 172