OAI/Computability/VertexCover/Repetition/SelectedMarginal.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.Repetition.selectedRawMarginal line 48
2. theorem OAI.UniqueGames.Foundations.Repetition.selectedPosterior_eq_raw line 56
3. theorem OAI.UniqueGames.Foundations.Repetition.selectedRawMarginal_firstMarginal line 84
4. theorem OAI.UniqueGames.Foundations.Repetition.selectedRawMarginal_isProbability line 95
5. theorem OAI.UniqueGames.Foundations.Repetition.selected_raw_information_bound line 113
6. def OAI.UniqueGames.Foundations.Repetition.selectedOutsideLikelihood line 128
7. def OAI.UniqueGames.Foundations.Repetition.selectedObservationEquiv line 136
8. theorem OAI.UniqueGames.Foundations.Repetition.selectedRawMarginal_fullReveal line 146
9. theorem OAI.UniqueGames.Foundations.Repetition.selectedRawReference_fullReveal line 163
10. theorem OAI.UniqueGames.Foundations.Repetition.selected_raw_error_eq_fullReveal line 179
11. theorem OAI.UniqueGames.Foundations.Repetition.selected_fullReveal_information_bound line 193
12. def OAI.UniqueGames.Foundations.Repetition.selectedInformationRadius line 207
13. theorem OAI.UniqueGames.Foundations.Repetition.selected_leftReveal_error_sum line 214
14. theorem OAI.UniqueGames.Foundations.Repetition.selected_rightReveal_error_sum line 237