OAI/Computability/VertexCover/Information/Tensorization.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.Information.coordinateMarginal line 45
  2. def OAI.UniqueGames.Foundations.Information.independentProduct line 49
  3. theorem OAI.UniqueGames.Foundations.Information.coordinateMarginal_isProbability line 51
  4. theorem OAI.UniqueGames.Foundations.Information.point_le_coordinateMarginal line 65
  5. theorem OAI.UniqueGames.Foundations.Information.marginal_expectation line 73
  6. theorem OAI.UniqueGames.Foundations.Information.independentProduct_isProbability line 82
  7. theorem OAI.UniqueGames.Foundations.Information.joint_supportedBy_product_coordinateMarginals line 90
  8. theorem OAI.UniqueGames.Foundations.Information.relativeEntropy_independent_reference line 98
  9. theorem OAI.UniqueGames.Foundations.Information.coordinate_relativeEntropy_sum_le line 141
  10. theorem OAI.UniqueGames.Foundations.Information.coordinate_totalVariation_sq_sum_le line 151
  11. theorem OAI.UniqueGames.Foundations.Information.posterior_coordinate_supportedBy line 160
  12. theorem OAI.UniqueGames.Foundations.Information.posterior_coordinate_totalVariation_sq_sum_le_log line 175
  13. theorem OAI.UniqueGames.Foundations.Information.posterior_coordinate_totalVariation_sum_le_sqrt line 188
  14. theorem OAI.UniqueGames.Foundations.Information.posterior_coordinate_totalVariation_sq_sum_le_binaryLog line 214