OAI/Combinatorics/IndependentSets/Repetition/MaskedVariation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Repetition.maskedJoint line 12
2. def OAI.IndependentSetsGames.Foundations.Repetition.maskedModel line 16
3. def OAI.IndependentSetsGames.Foundations.Repetition.leftRevealModel line 20
4. def OAI.IndependentSetsGames.Foundations.Repetition.rightRevealModel line 24
5. theorem OAI.IndependentSetsGames.Foundations.Repetition.sum_maskedJoint line 28
6. theorem OAI.IndependentSetsGames.Foundations.Repetition.maskedJoint_isProbability_iff line 44
7. theorem OAI.IndependentSetsGames.Foundations.Repetition.maskedJoint_firstMarginal_inl line 66
8. theorem OAI.IndependentSetsGames.Foundations.Repetition.maskedJoint_firstMarginal_inr line 75
9. theorem OAI.IndependentSetsGames.Foundations.Repetition.abs_half_sub_half_mul line 81
10. theorem OAI.IndependentSetsGames.Foundations.Repetition.abs_masked_inl line 87
11. theorem OAI.IndependentSetsGames.Foundations.Repetition.abs_masked_inr line 101
12. theorem OAI.IndependentSetsGames.Foundations.Repetition.masked_totalVariation_identity line 114
13. theorem OAI.IndependentSetsGames.Foundations.Repetition.leftRevealModel_totalVariation_le line 155
14. theorem OAI.IndependentSetsGames.Foundations.Repetition.rightRevealModel_totalVariation_le line 162