OAI/Computability/MinUncut/Games/Sampling.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.iid_pushforward line 10
  2. def OAI.MinUncutGames.Foundations.Games.FiniteDistribution.uniform line 30
  3. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.iid_uniform line 39
  4. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.expectation_uniform line 46
  5. instance OAI.MinUncut.Outer.equationFintype line 62
  6. def OAI.MinUncut.Outer.ordinaryAccepts line 69
  7. lemma OAI.MinUncut.Outer.ordinary_all_implies_satisfied line 72
  8. lemma OAI.MinUncut.Outer.ordinary_coordinate_bound line 81
  9. def OAI.MinUncut.Outer.equationFraction line 95
  10. def OAI.MinUncut.Outer.ordinaryGame line 100
  11. lemma OAI.MinUncut.Outer.ordinary_success_formula line 106
  12. lemma OAI.MinUncut.Outer.ordinary_success_le line 121
  13. theorem OAI.MinUncut.Outer.ordinary_value_le line 137
  14. def OAI.MinUncutGames.Foundations.Information.IsProbability line 155
  15. def OAI.MinUncutGames.Foundations.Information.SupportedBy line 158
  16. def OAI.MinUncutGames.Foundations.Information.relativeEntropy line 160
  17. def OAI.MinUncutGames.Foundations.Information.totalVariation line 163
  18. def OAI.MinUncutGames.Foundations.Information.posterior line 166
  19. theorem OAI.MinUncutGames.Foundations.Information.posterior_isProbability line 169
  20. theorem OAI.MinUncutGames.Foundations.Information.posterior_supportedBy line 179
  21. theorem OAI.MinUncutGames.Foundations.Information.mul_log_div_ge_sub line 184
  22. theorem OAI.MinUncutGames.Foundations.Information.relativeEntropy_nonneg line 192
  23. theorem OAI.MinUncutGames.Foundations.Information.posterior_relativeEntropy_le line 204
  24. theorem OAI.MinUncutGames.Foundations.Information.totalVariation_nonneg line 228
  25. theorem OAI.MinUncutGames.Foundations.Information.totalVariation_symm line 231
  26. theorem OAI.MinUncutGames.Foundations.Information.totalVariation_le_one line 234
  27. theorem OAI.MinUncutGames.Foundations.Information.le_binaryLog_of_le_log line 245
  28. theorem OAI.MinUncutGames.Foundations.Information.weighted_sum_sq_le line 255
  29. def OAI.MinUncutGames.Foundations.Information.firstMarginal line 271
  30. def OAI.MinUncutGames.Foundations.Information.secondMarginal line 273
  31. def OAI.MinUncutGames.Foundations.Information.product line 275
  32. theorem OAI.MinUncutGames.Foundations.Information.firstMarginal_isProbability line 277
  33. theorem OAI.MinUncutGames.Foundations.Information.secondMarginal_isProbability line 284
  34. theorem OAI.MinUncutGames.Foundations.Information.product_isProbability line 293
  35. theorem OAI.MinUncutGames.Foundations.Information.point_le_firstMarginal line 300
  36. theorem OAI.MinUncutGames.Foundations.Information.point_le_secondMarginal line 305
  37. theorem OAI.MinUncutGames.Foundations.Information.joint_supportedBy_product_marginals line 310
  38. theorem OAI.MinUncutGames.Foundations.Information.relativeEntropy_product_reference line 318
  39. theorem OAI.MinUncutGames.Foundations.Information.marginal_relativeEntropy_sum_le line 352
  40. def OAI.MinUncutGames.Foundations.Information.conditionalKernel line 363
  41. theorem OAI.MinUncutGames.Foundations.Information.conditionalKernel_isProbability line 369
  42. theorem OAI.MinUncutGames.Foundations.Information.marginal_mul_conditionalKernel line 385
  43. theorem OAI.MinUncutGames.Foundations.Information.law_of_total_probability line 402
  44. theorem OAI.MinUncutGames.Foundations.Information.kernelProduct_isProbability line 409
  45. theorem OAI.MinUncutGames.Foundations.Information.alternativeInput_conditionalProduct_isProbability line 419
  46. theorem OAI.MinUncutGames.Foundations.Information.totalVariation_joint_common_weights line 428
  47. theorem OAI.MinUncutGames.Foundations.Information.totalVariation_joint_common_kernel line 439
  48. theorem OAI.MinUncutGames.Foundations.Information.totalVariation_condition_le line 449
  49. theorem OAI.MinUncutGames.Foundations.Information.weighted_coordinate_sum_sq_le line 468