OAI/Computability/MinUncut/Games/TotalVariation.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.Games.FiniteDistribution.totalVariation line 13
  2. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.totalVariation_nonnegative line 16
  3. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.totalVariation_comm line 20
  4. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.probability_sub_le_totalVariation line 28
  5. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.probability_abs_sub_le_totalVariation line 44
  6. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.probability_le_add_totalVariation line 54
  7. def OAI.MinUncutGames.Foundations.Games.FiniteDistribution.condition line 73
  8. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.probability_condition line 89
  9. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.probability_inter_eq_mul_conditional line 98
  10. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.probability_and_le_left line 106
  11. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.probability_and_le_right line 113
  12. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.probability_and_eq_zero_of_probability_eq_zero line 120
  13. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.probability_condition_given line 127
  14. theorem OAI.MinUncutGames.Foundations.Games.Game.selectedWins_insert line 141
  15. def OAI.MinUncutGames.Foundations.Games.Game.selectedSuccess line 152
  16. theorem OAI.MinUncutGames.Foundations.Games.Game.selectedSuccess_nonnegative line 157
  17. theorem OAI.MinUncutGames.Foundations.Games.Game.selectedSuccess_le_one line 162
  18. theorem OAI.MinUncutGames.Foundations.Games.Game.selectedSuccess_empty line 167
  19. theorem OAI.MinUncutGames.Foundations.Games.Game.selectedSuccess_univ line 174
  20. theorem OAI.MinUncutGames.Foundations.Games.Game.selectedSuccess_antitone line 180
  21. theorem OAI.MinUncutGames.Foundations.Games.Game.selectedSuccess_insert line 186
  22. theorem OAI.MinUncutGames.Foundations.Games.Game.selectedSuccess_insert_eq_zero line 198
  23. theorem OAI.MinUncutGames.Foundations.Information.gameLaw_isProbability line 219
  24. def OAI.MinUncutGames.Foundations.Information.toGameLaw line 222
  25. def OAI.MinUncutGames.Foundations.Information.gameLawEquiv line 227
  26. theorem OAI.MinUncutGames.Foundations.Information.totalVariation_gameLaw line 233
  27. def OAI.MinUncutGames.Foundations.Information.gameConditionalKernel line 236
  28. theorem OAI.MinUncutGames.Foundations.Information.gameConditionalKernel_recombine line 242
  29. def OAI.MinUncutGames.Foundations.Information.gameConditionalProduct line 248
  30. theorem OAI.MinUncutGames.Foundations.Information.gameConditionalProduct_weight line 255
  31. theorem OAI.MinUncutGames.Foundations.Information.gameCondition_weight line 261
  32. theorem OAI.MinUncutGames.Foundations.Information.gameCondition_relativeEntropy_le line 268