OAI/Computability/VertexCover/Information/ChainRule.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.Information.firstMarginal line 45
2. def OAI.UniqueGames.Foundations.Information.secondMarginal line 47
3. def OAI.UniqueGames.Foundations.Information.product line 49
4. theorem OAI.UniqueGames.Foundations.Information.firstMarginal_isProbability line 51
5. theorem OAI.UniqueGames.Foundations.Information.secondMarginal_isProbability line 58
6. theorem OAI.UniqueGames.Foundations.Information.product_isProbability line 67
7. theorem OAI.UniqueGames.Foundations.Information.point_le_firstMarginal line 74
8. theorem OAI.UniqueGames.Foundations.Information.point_le_secondMarginal line 79
9. theorem OAI.UniqueGames.Foundations.Information.joint_supportedBy_product_marginals line 84
10. theorem OAI.UniqueGames.Foundations.Information.relativeEntropy_product_reference line 92
11. theorem OAI.UniqueGames.Foundations.Information.marginal_relativeEntropy_sum_le line 126