OAI/Combinatorics/IndependentSets/Repetition/SelectedInformation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Repetition.mergeCoordinates line 12
2. def OAI.IndependentSetsGames.Foundations.Repetition.coordinateSplitEquiv line 16
3. theorem OAI.IndependentSetsGames.Foundations.Repetition.iid_coordinate_split line 24
4. abbrev OAI.IndependentSetsGames.Foundations.Repetition.SelectedLabels line 54
5. def OAI.IndependentSetsGames.Foundations.Repetition.selectedQuestionTuple line 57
6. def OAI.IndependentSetsGames.Foundations.Repetition.selectedAnswerLabel line 64
7. def OAI.IndependentSetsGames.Foundations.Repetition.selectedLikelihood line 70
8. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedLikelihood_nonnegative line 81
9. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedLikelihood_sum line 92
10. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedLikelihood_sum_le_one line 103
11. def OAI.IndependentSetsGames.Foundations.Repetition.selectedSplitLaw line 111
12. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedSplit_probability line 118
13. abbrev OAI.IndependentSetsGames.Foundations.Repetition.SelectedInput line 134
14. def OAI.IndependentSetsGames.Foundations.Repetition.selectedInputLaw line 137
15. def OAI.IndependentSetsGames.Foundations.Repetition.selectedInputProfile line 142
16. def OAI.IndependentSetsGames.Foundations.Repetition.selectedSideMass line 146
17. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedSideMass_sum line 154
18. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedSideMass_total line 166
19. def OAI.IndependentSetsGames.Foundations.Repetition.selectedSideWeight line 188
20. theorem OAI.IndependentSetsGames.Foundations.Repetition.selected_information_bound line 195