OAI/Combinatorics/IndependentSets/Repetition/SelectedJoint.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Repetition.selectedJointWeight line 17
2. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedJointWeight_nonnegative line 28
3. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedJointWeight_firstMarginal line 40
4. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedJointWeight_isProbability line 51
5. def OAI.IndependentSetsGames.Foundations.Repetition.selectedJointLaw line 62
6. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedJointWeight_factorization line 68
7. theorem OAI.IndependentSetsGames.Foundations.Repetition.totalVariation_triangle line 89
8. def OAI.IndependentSetsGames.Foundations.Repetition.conditionWeights line 100
9. theorem OAI.IndependentSetsGames.Foundations.Repetition.conditionWeights_isProbability line 103
10. theorem OAI.IndependentSetsGames.Foundations.Repetition.totalVariation_condition_le line 120
11. theorem OAI.IndependentSetsGames.Foundations.Repetition.totalVariation_condition_half_le line 143
12. theorem OAI.IndependentSetsGames.Foundations.Repetition.totalVariation_append_kernel line 150
13. def OAI.IndependentSetsGames.Foundations.Repetition.kernelPushforward line 163
14. theorem OAI.IndependentSetsGames.Foundations.Repetition.totalVariation_kernelPushforward_le line 166