OAI/Combinatorics/IndependentSets/Repetition/PartialReveal.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Repetition.mergeAt line 12
2. theorem OAI.IndependentSetsGames.Foundations.Repetition.mergeAt_self line 16
3. theorem OAI.IndependentSetsGames.Foundations.Repetition.mergeAt_other line 20
4. def OAI.IndependentSetsGames.Foundations.Repetition.partialRevealWeight line 24
5. theorem OAI.IndependentSetsGames.Foundations.Repetition.product_reveal_at line 28
6. def OAI.IndependentSetsGames.Foundations.Repetition.partialRevealMarginal line 38
7. def OAI.IndependentSetsGames.Foundations.Repetition.fullRevealMarginal line 45
8. theorem OAI.IndependentSetsGames.Foundations.Repetition.fullRevealMarginal_merge line 53
9. def OAI.IndependentSetsGames.Foundations.Repetition.fullRevealModel line 79
10. theorem OAI.IndependentSetsGames.Foundations.Repetition.fullRevealModel_merge line 86
11. def OAI.IndependentSetsGames.Foundations.Repetition.revealSplitEquiv line 94
12. theorem OAI.IndependentSetsGames.Foundations.Repetition.totalVariation_comp_equiv line 116
13. theorem OAI.IndependentSetsGames.Foundations.Repetition.fullReveal_totalVariation line 124
14. theorem OAI.IndependentSetsGames.Foundations.Repetition.leftReveal_full_error line 139
15. theorem OAI.IndependentSetsGames.Foundations.Repetition.rightReveal_full_error line 148