OAI/Combinatorics/IndependentSets/Repetition/Pinsker.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Information.hellingerSquared line 14
  2. theorem OAI.IndependentSetsGames.Foundations.Information.sqrt_distance_le_relativeEntropy_term line 17
  3. theorem OAI.IndependentSetsGames.Foundations.Information.hellingerSquared_le_relativeEntropy line 42
  4. theorem OAI.IndependentSetsGames.Foundations.Information.totalVariation_sq_le_hellingerSquared line 50
  5. theorem OAI.IndependentSetsGames.Foundations.Information.totalVariation_sq_le_relativeEntropy line 75
  6. theorem OAI.IndependentSetsGames.Foundations.Information.posterior_totalVariation_sq_le_log line 81
  7. def OAI.IndependentSetsGames.Foundations.Information.coordinateMarginal line 95
  8. def OAI.IndependentSetsGames.Foundations.Information.independentProduct line 99
  9. theorem OAI.IndependentSetsGames.Foundations.Information.coordinateMarginal_isProbability line 101
  10. theorem OAI.IndependentSetsGames.Foundations.Information.point_le_coordinateMarginal line 115
  11. theorem OAI.IndependentSetsGames.Foundations.Information.marginal_expectation line 123
  12. theorem OAI.IndependentSetsGames.Foundations.Information.independentProduct_isProbability line 132
  13. theorem OAI.IndependentSetsGames.Foundations.Information.joint_supportedBy_product_coordinateMarginals line 140
  14. theorem OAI.IndependentSetsGames.Foundations.Information.relativeEntropy_independent_reference line 148
  15. theorem OAI.IndependentSetsGames.Foundations.Information.coordinate_relativeEntropy_sum_le line 193
  16. theorem OAI.IndependentSetsGames.Foundations.Information.coordinate_totalVariation_sq_sum_le line 203
  17. theorem OAI.IndependentSetsGames.Foundations.Information.posterior_coordinate_supportedBy line 212
  18. theorem OAI.IndependentSetsGames.Foundations.Information.posterior_coordinate_totalVariation_sq_sum_le_log line 227
  19. theorem OAI.IndependentSetsGames.Foundations.Information.posterior_coordinate_totalVariation_sum_le_sqrt line 240
  20. theorem OAI.IndependentSetsGames.Foundations.Information.posterior_coordinate_totalVariation_sq_sum_le_binaryLog line 266