OAI/Computability/BinPacking/Information/GamesAdapter.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGames.Foundations.Information.IsProbability line 19
  2. def OAI.BinPackingGames.Foundations.Information.SupportedBy line 22
  3. def OAI.BinPackingGames.Foundations.Information.relativeEntropy line 24
  4. def OAI.BinPackingGames.Foundations.Information.totalVariation line 27
  5. def OAI.BinPackingGames.Foundations.Information.posterior line 30
  6. theorem OAI.BinPackingGames.Foundations.Information.posterior_isProbability line 33
  7. theorem OAI.BinPackingGames.Foundations.Information.posterior_supportedBy line 43
  8. theorem OAI.BinPackingGames.Foundations.Information.mul_log_div_ge_sub line 48
  9. theorem OAI.BinPackingGames.Foundations.Information.relativeEntropy_nonneg line 56
  10. theorem OAI.BinPackingGames.Foundations.Information.posterior_relativeEntropy_le line 68
  11. theorem OAI.BinPackingGames.Foundations.Information.totalVariation_nonneg line 92
  12. theorem OAI.BinPackingGames.Foundations.Information.totalVariation_symm line 95
  13. theorem OAI.BinPackingGames.Foundations.Information.totalVariation_le_one line 98
  14. theorem OAI.BinPackingGames.Foundations.Information.le_binaryLog_of_le_log line 109
  15. theorem OAI.BinPackingGames.Foundations.Information.weighted_sum_sq_le line 119
  16. def OAI.BinPackingGames.Foundations.Information.firstMarginal line 139
  17. def OAI.BinPackingGames.Foundations.Information.secondMarginal line 141
  18. def OAI.BinPackingGames.Foundations.Information.product line 143
  19. theorem OAI.BinPackingGames.Foundations.Information.firstMarginal_isProbability line 145
  20. theorem OAI.BinPackingGames.Foundations.Information.secondMarginal_isProbability line 152
  21. theorem OAI.BinPackingGames.Foundations.Information.product_isProbability line 161
  22. theorem OAI.BinPackingGames.Foundations.Information.point_le_firstMarginal line 168
  23. theorem OAI.BinPackingGames.Foundations.Information.point_le_secondMarginal line 173
  24. theorem OAI.BinPackingGames.Foundations.Information.joint_supportedBy_product_marginals line 178
  25. theorem OAI.BinPackingGames.Foundations.Information.relativeEntropy_product_reference line 186
  26. theorem OAI.BinPackingGames.Foundations.Information.marginal_relativeEntropy_sum_le line 220
  27. theorem OAI.BinPackingGames.Foundations.Information.totalVariation_joint_common_weights line 231
  28. theorem OAI.BinPackingGames.Foundations.Information.totalVariation_joint_common_kernel line 242
  29. theorem OAI.BinPackingGames.Foundations.Information.totalVariation_condition_le line 252
  30. theorem OAI.BinPackingGames.Foundations.Information.weighted_coordinate_sum_sq_le line 271
  31. def OAI.BinPackingGames.Foundations.Information.hellingerSquared line 311
  32. theorem OAI.BinPackingGames.Foundations.Information.sqrt_distance_le_relativeEntropy_term line 314
  33. theorem OAI.BinPackingGames.Foundations.Information.hellingerSquared_le_relativeEntropy line 339
  34. theorem OAI.BinPackingGames.Foundations.Information.totalVariation_sq_le_hellingerSquared line 347
  35. theorem OAI.BinPackingGames.Foundations.Information.totalVariation_sq_le_relativeEntropy line 372
  36. theorem OAI.BinPackingGames.Foundations.Information.posterior_totalVariation_sq_le_log line 378
  37. theorem OAI.BinPackingGames.Foundations.Information.normalize_isProbability line 386
  38. theorem OAI.BinPackingGames.Foundations.Information.relativeEntropy_normalize_right line 394
  39. theorem OAI.BinPackingGames.Foundations.Information.neg_relativeEntropy_le_log_mass line 408
  40. theorem OAI.BinPackingGames.Foundations.Information.posterior_weighted_log_inverse_le line 418
  41. def OAI.BinPackingGames.Foundations.Information.conditionalKernel line 456
  42. theorem OAI.BinPackingGames.Foundations.Information.conditionalKernel_isProbability line 462
  43. theorem OAI.BinPackingGames.Foundations.Information.marginal_mul_conditionalKernel line 478
  44. theorem OAI.BinPackingGames.Foundations.Information.law_of_total_probability line 495
  45. theorem OAI.BinPackingGames.Foundations.Information.kernelProduct_isProbability line 502
  46. theorem OAI.BinPackingGames.Foundations.Information.alternativeInput_conditionalProduct_isProbability line 512
  47. theorem OAI.BinPackingGames.Foundations.Information.gameLaw_isProbability line 521
  48. def OAI.BinPackingGames.Foundations.Information.toGameLaw line 524
  49. def OAI.BinPackingGames.Foundations.Information.gameLawEquiv line 529
  50. theorem OAI.BinPackingGames.Foundations.Information.totalVariation_gameLaw line 535
  51. def OAI.BinPackingGames.Foundations.Information.gameConditionalKernel line 538
  52. theorem OAI.BinPackingGames.Foundations.Information.gameConditionalKernel_recombine line 544
  53. def OAI.BinPackingGames.Foundations.Information.gameConditionalProduct line 550
  54. theorem OAI.BinPackingGames.Foundations.Information.gameConditionalProduct_weight line 557
  55. theorem OAI.BinPackingGames.Foundations.Information.gameCondition_weight line 563
  56. theorem OAI.BinPackingGames.Foundations.Information.gameCondition_relativeEntropy_le line 570