OAI/Combinatorics/IndependentSets/Repetition/SelectedMarginal.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Repetition.selectedRawMarginal line 15
2. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedPosterior_eq_raw line 23
3. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedRawMarginal_firstMarginal line 51
4. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedRawMarginal_isProbability line 62
5. theorem OAI.IndependentSetsGames.Foundations.Repetition.selected_raw_information_bound line 80
6. def OAI.IndependentSetsGames.Foundations.Repetition.selectedOutsideLikelihood line 95
7. def OAI.IndependentSetsGames.Foundations.Repetition.selectedObservationEquiv line 103
8. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedRawMarginal_fullReveal line 113
9. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedRawReference_fullReveal line 130
10. theorem OAI.IndependentSetsGames.Foundations.Repetition.selected_raw_error_eq_fullReveal line 146
11. theorem OAI.IndependentSetsGames.Foundations.Repetition.selected_fullReveal_information_bound line 160
12. def OAI.IndependentSetsGames.Foundations.Repetition.selectedInformationRadius line 174
13. theorem OAI.IndependentSetsGames.Foundations.Repetition.selected_leftReveal_error_sum line 181
14. theorem OAI.IndependentSetsGames.Foundations.Repetition.selected_rightReveal_error_sum line 204