OAI/Combinatorics/IndependentSets/Repetition/Finite.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Information.IsProbability line 13
  2. def OAI.IndependentSetsGames.Foundations.Information.SupportedBy line 16
  3. def OAI.IndependentSetsGames.Foundations.Information.relativeEntropy line 18
  4. def OAI.IndependentSetsGames.Foundations.Information.totalVariation line 21
  5. def OAI.IndependentSetsGames.Foundations.Information.posterior line 24
  6. theorem OAI.IndependentSetsGames.Foundations.Information.posterior_isProbability line 27
  7. theorem OAI.IndependentSetsGames.Foundations.Information.posterior_supportedBy line 37
  8. theorem OAI.IndependentSetsGames.Foundations.Information.mul_log_div_ge_sub line 42
  9. theorem OAI.IndependentSetsGames.Foundations.Information.relativeEntropy_nonneg line 50
  10. theorem OAI.IndependentSetsGames.Foundations.Information.posterior_relativeEntropy_le line 62
  11. theorem OAI.IndependentSetsGames.Foundations.Information.totalVariation_nonneg line 86
  12. theorem OAI.IndependentSetsGames.Foundations.Information.totalVariation_symm line 89
  13. theorem OAI.IndependentSetsGames.Foundations.Information.totalVariation_le_one line 92
  14. theorem OAI.IndependentSetsGames.Foundations.Information.le_binaryLog_of_le_log line 103
  15. theorem OAI.IndependentSetsGames.Foundations.Information.weighted_sum_sq_le line 113
  16. def OAI.IndependentSetsGames.Foundations.Information.firstMarginal line 131
  17. def OAI.IndependentSetsGames.Foundations.Information.secondMarginal line 133
  18. def OAI.IndependentSetsGames.Foundations.Information.product line 135
  19. theorem OAI.IndependentSetsGames.Foundations.Information.firstMarginal_isProbability line 137
  20. theorem OAI.IndependentSetsGames.Foundations.Information.secondMarginal_isProbability line 144
  21. theorem OAI.IndependentSetsGames.Foundations.Information.product_isProbability line 153
  22. theorem OAI.IndependentSetsGames.Foundations.Information.point_le_firstMarginal line 160
  23. theorem OAI.IndependentSetsGames.Foundations.Information.point_le_secondMarginal line 165
  24. theorem OAI.IndependentSetsGames.Foundations.Information.joint_supportedBy_product_marginals line 170
  25. theorem OAI.IndependentSetsGames.Foundations.Information.relativeEntropy_product_reference line 178
  26. theorem OAI.IndependentSetsGames.Foundations.Information.marginal_relativeEntropy_sum_le line 212