OAI/Combinatorics/IndependentSets/Repetition/TotalVariation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.totalVariation line 14
2. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.totalVariation_nonnegative line 17
3. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.totalVariation_comm line 21
4. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.probability_sub_le_totalVariation line 29
5. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.probability_abs_sub_le_totalVariation line 45
6. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.probability_le_add_totalVariation line 55
7. theorem OAI.IndependentSetsGames.Foundations.Information.gameLaw_isProbability line 70
8. def OAI.IndependentSetsGames.Foundations.Information.toGameLaw line 73
9. def OAI.IndependentSetsGames.Foundations.Information.gameLawEquiv line 78
10. theorem OAI.IndependentSetsGames.Foundations.Information.totalVariation_gameLaw line 84
11. def OAI.IndependentSetsGames.Foundations.Information.gameConditionalKernel line 87
12. theorem OAI.IndependentSetsGames.Foundations.Information.gameConditionalKernel_recombine line 93
13. def OAI.IndependentSetsGames.Foundations.Information.gameConditionalProduct line 99
14. theorem OAI.IndependentSetsGames.Foundations.Information.gameConditionalProduct_weight line 106
15. theorem OAI.IndependentSetsGames.Foundations.Information.gameCondition_weight line 112
16. theorem OAI.IndependentSetsGames.Foundations.Information.gameCondition_relativeEntropy_le line 119