OAI/Computability/MinUncut/PCP/SelectedMarginal.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.Repetition.selectedRawMarginal line 14
2. theorem OAI.MinUncutGames.Foundations.Repetition.selectedPosterior_eq_raw line 22
3. theorem OAI.MinUncutGames.Foundations.Repetition.selectedRawMarginal_firstMarginal line 50
4. theorem OAI.MinUncutGames.Foundations.Repetition.selectedRawMarginal_isProbability line 61
5. theorem OAI.MinUncutGames.Foundations.Repetition.selected_raw_information_bound line 79
6. def OAI.MinUncutGames.Foundations.Repetition.selectedOutsideLikelihood line 94
7. def OAI.MinUncutGames.Foundations.Repetition.selectedObservationEquiv line 102
8. theorem OAI.MinUncutGames.Foundations.Repetition.selectedRawMarginal_fullReveal line 112
9. theorem OAI.MinUncutGames.Foundations.Repetition.selectedRawReference_fullReveal line 129
10. theorem OAI.MinUncutGames.Foundations.Repetition.selected_raw_error_eq_fullReveal line 145
11. theorem OAI.MinUncutGames.Foundations.Repetition.selected_fullReveal_information_bound line 159
12. def OAI.MinUncutGames.Foundations.Repetition.selectedInformationRadius line 173
13. theorem OAI.MinUncutGames.Foundations.Repetition.selected_leftReveal_error_sum line 180
14. theorem OAI.MinUncutGames.Foundations.Repetition.selected_rightReveal_error_sum line 203
15. theorem OAI.MinUncutGames.Foundations.Repetition.selectedSplit_question_probability line 228
16. theorem OAI.MinUncutGames.Foundations.Repetition.selectedJoint_eventMass line 244
17. theorem OAI.MinUncutGames.Foundations.Repetition.selectedJointLaw_question_probability line 290
18. theorem OAI.MinUncutGames.Foundations.Repetition.selectedJointLaw_questions_pushforward line 328
19. def OAI.MinUncutGames.Foundations.Repetition.selectedTupleLikelihood line 349
20. theorem OAI.MinUncutGames.Foundations.Repetition.selectedTupleLikelihood_nonnegative line 355
21. theorem OAI.MinUncutGames.Foundations.Repetition.selectedTupleLikelihood_le_one line 363
22. theorem OAI.MinUncutGames.Foundations.Repetition.selectedTupleLikelihood_mass line 371
23. def OAI.MinUncutGames.Foundations.Repetition.selectedQuestionMarginal line 384
24. theorem OAI.MinUncutGames.Foundations.Repetition.selectedQuestionMarginal_weight line 391
25. theorem OAI.MinUncutGames.Foundations.Repetition.selectedQuestionMarginal_totalVariation_sq_sum_le_log line 409
26. theorem OAI.MinUncutGames.Foundations.Repetition.unselectedQuestionMarginal_totalVariation_sq_sum_le_log line 427
27. theorem OAI.MinUncutGames.Foundations.Repetition.unselectedQuestionMarginal_totalVariation_sum_le_sqrt line 449
28. theorem OAI.MinUncutGames.Foundations.Repetition.unselectedQuestionMarginal_totalVariation_sum_le_sqrt_sub_card line 477