OAI/Computability/BinPacking/Information/SideInformation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGames.Foundations.Information.coordinateMarginal line 15
  2. def OAI.BinPackingGames.Foundations.Information.independentProduct line 19
  3. theorem OAI.BinPackingGames.Foundations.Information.coordinateMarginal_isProbability line 21
  4. theorem OAI.BinPackingGames.Foundations.Information.point_le_coordinateMarginal line 35
  5. theorem OAI.BinPackingGames.Foundations.Information.marginal_expectation line 43
  6. theorem OAI.BinPackingGames.Foundations.Information.independentProduct_isProbability line 52
  7. theorem OAI.BinPackingGames.Foundations.Information.joint_supportedBy_product_coordinateMarginals line 60
  8. theorem OAI.BinPackingGames.Foundations.Information.relativeEntropy_independent_reference line 68
  9. theorem OAI.BinPackingGames.Foundations.Information.coordinate_relativeEntropy_sum_le line 111
  10. theorem OAI.BinPackingGames.Foundations.Information.coordinate_totalVariation_sq_sum_le line 121
  11. theorem OAI.BinPackingGames.Foundations.Information.posterior_coordinate_supportedBy line 130
  12. theorem OAI.BinPackingGames.Foundations.Information.posterior_coordinate_totalVariation_sq_sum_le_log line 145
  13. theorem OAI.BinPackingGames.Foundations.Information.posterior_coordinate_totalVariation_sum_le_sqrt line 158
  14. theorem OAI.BinPackingGames.Foundations.Information.posterior_coordinate_totalVariation_sq_sum_le_binaryLog line 184
  15. def OAI.BinPackingGames.Foundations.Information.posteriorOrOriginal line 198
  16. theorem OAI.BinPackingGames.Foundations.Information.posteriorOrOriginal_isProbability line 203
  17. theorem OAI.BinPackingGames.Foundations.Information.mass_mul_posteriorOrOriginal line 214
  18. theorem OAI.BinPackingGames.Foundations.Information.weighted_coordinate_posterior_recombine line 234
  19. theorem OAI.BinPackingGames.Foundations.Information.side_information_bound line 256
  20. theorem OAI.BinPackingGames.Foundations.Information.finite_side_information_bound line 324