OAI/Computability/MinUncut/Games/Pinsker.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.Information.hellingerSquared line 12
  2. theorem OAI.MinUncutGames.Foundations.Information.sqrt_distance_le_relativeEntropy_term line 15
  3. theorem OAI.MinUncutGames.Foundations.Information.hellingerSquared_le_relativeEntropy line 40
  4. theorem OAI.MinUncutGames.Foundations.Information.totalVariation_sq_le_hellingerSquared line 48
  5. theorem OAI.MinUncutGames.Foundations.Information.totalVariation_sq_le_relativeEntropy line 73
  6. theorem OAI.MinUncutGames.Foundations.Information.posterior_totalVariation_sq_le_log line 79
  7. def OAI.MinUncutGames.Foundations.Information.coordinateMarginal line 91
  8. def OAI.MinUncutGames.Foundations.Information.independentProduct line 95
  9. theorem OAI.MinUncutGames.Foundations.Information.coordinateMarginal_isProbability line 97
  10. theorem OAI.MinUncutGames.Foundations.Information.point_le_coordinateMarginal line 111
  11. theorem OAI.MinUncutGames.Foundations.Information.marginal_expectation line 119
  12. theorem OAI.MinUncutGames.Foundations.Information.independentProduct_isProbability line 128
  13. theorem OAI.MinUncutGames.Foundations.Information.joint_supportedBy_product_coordinateMarginals line 136
  14. theorem OAI.MinUncutGames.Foundations.Information.relativeEntropy_independent_reference line 144
  15. theorem OAI.MinUncutGames.Foundations.Information.coordinate_relativeEntropy_sum_le line 187
  16. theorem OAI.MinUncutGames.Foundations.Information.coordinate_totalVariation_sq_sum_le line 197
  17. theorem OAI.MinUncutGames.Foundations.Information.posterior_coordinate_supportedBy line 206
  18. theorem OAI.MinUncutGames.Foundations.Information.posterior_coordinate_totalVariation_sq_sum_le_log line 221
  19. theorem OAI.MinUncutGames.Foundations.Information.posterior_coordinate_totalVariation_sum_le_sqrt line 234
  20. theorem OAI.MinUncutGames.Foundations.Information.posterior_coordinate_totalVariation_sq_sum_le_binaryLog line 260
  21. theorem OAI.MinUncutGames.Foundations.Information.normalize_isProbability line 274
  22. theorem OAI.MinUncutGames.Foundations.Information.relativeEntropy_normalize_right line 282
  23. theorem OAI.MinUncutGames.Foundations.Information.neg_relativeEntropy_le_log_mass line 296
  24. theorem OAI.MinUncutGames.Foundations.Information.posterior_weighted_log_inverse_le line 306
  25. def OAI.MinUncutGames.Foundations.Information.posteriorOrOriginal line 340
  26. theorem OAI.MinUncutGames.Foundations.Information.posteriorOrOriginal_isProbability line 345
  27. theorem OAI.MinUncutGames.Foundations.Information.mass_mul_posteriorOrOriginal line 356
  28. theorem OAI.MinUncutGames.Foundations.Information.weighted_coordinate_posterior_recombine line 376
  29. theorem OAI.MinUncutGames.Foundations.Information.side_information_bound line 398
  30. theorem OAI.MinUncutGames.Foundations.Information.finite_side_information_bound line 466