OAI/Computability/DirectedFeedback/Probability/Basic.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.DFVSGames.Foundations.Games.FiniteDistribution line 12
  2. def OAI.DFVSGames.Foundations.Games.FiniteDistribution.expectation line 21
  3. def OAI.DFVSGames.Foundations.Games.FiniteDistribution.probability line 24
  4. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.probability_nonnegative line 27
  5. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.probability_le_one line 35
  6. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.probability_true line 44
  7. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.probability_false line 48
  8. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.probability_mono line 52
  9. def OAI.DFVSGames.Foundations.Games.FiniteDistribution.pushforward line 64
  10. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.probability_pushforward line 76
  11. def OAI.DFVSGames.Foundations.Games.FiniteDistribution.transport line 88
  12. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.probability_transport line 93
  13. def OAI.DFVSGames.Foundations.Games.FiniteDistribution.iid line 99
  14. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.probability_iid_all line 104
  15. abbrev OAI.DFVSGames.Foundations.Games.Strategy line 123
  16. structure OAI.DFVSGames.Foundations.Games.Game line 125
  17. def OAI.DFVSGames.Foundations.Games.Game.wins line 135
  18. def OAI.DFVSGames.Foundations.Games.Game.success line 139
  19. theorem OAI.DFVSGames.Foundations.Games.Game.success_nonnegative line 142
  20. theorem OAI.DFVSGames.Foundations.Games.Game.success_le_one line 146
  21. def OAI.DFVSGames.Foundations.Games.Game.simulatedStrategy line 150
  22. theorem OAI.DFVSGames.Foundations.Games.Game.success_le_of_localSimulation line 157
  23. def OAI.DFVSGames.Foundations.Games.Game.tupleQuestionEquiv line 176
  24. def OAI.DFVSGames.Foundations.Games.Game.repetition line 183
  25. def OAI.DFVSGames.Foundations.Games.Game.repeatStrategy line 190
  26. theorem OAI.DFVSGames.Foundations.Games.Game.success_repeatStrategy line 194
  27. theorem OAI.DFVSGames.Foundations.Games.Game.repetition_question_weight line 202
  28. theorem OAI.DFVSGames.Foundations.Games.Game.repetition_accepts_iff line 207
  29. def OAI.DFVSGames.Foundations.Games.Game.coordinateWin line 214
  30. def OAI.DFVSGames.Foundations.Games.Game.selectedWins line 220
  31. theorem OAI.DFVSGames.Foundations.Games.Game.selectedWins_mono line 226
  32. theorem OAI.DFVSGames.Foundations.Games.Game.selectedWins_empty line 237
  33. theorem OAI.DFVSGames.Foundations.Games.Game.selectedWins_univ line 243
  34. def OAI.DFVSGames.Foundations.Games.Game.value line 269
  35. theorem OAI.DFVSGames.Foundations.Games.Game.success_le_value line 273
  36. theorem OAI.DFVSGames.Foundations.Games.Game.value_le_iff line 278
  37. theorem OAI.DFVSGames.Foundations.Games.Game.exists_optimal_strategy line 283
  38. theorem OAI.DFVSGames.Foundations.Games.Game.value_nonnegative line 290
  39. theorem OAI.DFVSGames.Foundations.Games.Game.value_le_one line 295
  40. theorem OAI.DFVSGames.Foundations.Games.Game.randomized_success_le_value line 298
  41. theorem OAI.DFVSGames.Foundations.Games.Game.success_repetition_zero line 311
  42. theorem OAI.DFVSGames.Foundations.Games.Game.value_repetition_zero line 320
  43. theorem OAI.DFVSGames.Foundations.Games.Game.pow_value_le_repetition_value line 326
  44. theorem OAI.DFVSGames.Foundations.Games.Game.value_le_of_localSimulation line 332
  45. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.eq_of_weight_eq line 363
  46. def OAI.DFVSGames.Foundations.Games.FiniteDistribution.table line 373
  47. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.expectation_table_eval line 384
  48. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.table_eval_pushforward line 412
  49. def OAI.DFVSGames.Foundations.Games.FiniteDistribution.product line 426
  50. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.expectation_product line 435
  51. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.expectation_comm line 441
  52. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.expectation_congr line 454
  53. def OAI.DFVSGames.Foundations.Games.Game.responseTableLaw line 467
  54. def OAI.DFVSGames.Foundations.Games.Game.stochasticSuccess line 473
  55. theorem OAI.DFVSGames.Foundations.Games.Game.success_eq_question_expectation line 482
  56. theorem OAI.DFVSGames.Foundations.Games.Game.table_success_eq_stochastic line 489
  57. theorem OAI.DFVSGames.Foundations.Games.Game.stochasticSuccess_le_value line 527
  58. theorem OAI.DFVSGames.Foundations.Games.Game.exists_deterministic_ge_stochastic line 535
  59. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.iid_pushforward line 553
  60. def OAI.DFVSGames.Foundations.Games.FiniteDistribution.uniform line 573
  61. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.iid_uniform line 582
  62. theorem OAI.DFVSGames.Foundations.Games.FiniteDistribution.expectation_uniform line 589
  63. def OAI.DFVSGames.Repetition.IsProjection line 610
  64. theorem OAI.DFVSGames.Repetition.IsProjection.of_accepts_iff line 614
  65. theorem OAI.DFVSGames.Repetition.IsProjection.repetition line 621
  66. def OAI.DFVSGames.Repetition.ofProjection line 629
  67. theorem OAI.DFVSGames.Repetition.ofProjection_accepts_iff line 634
  68. theorem OAI.DFVSGames.Repetition.ofProjection_isProjection line 641
  69. def OAI.DFVSGames.Repetition.productQuestionEquiv line 645
  70. def OAI.DFVSGames.Repetition.product line 652
  71. theorem OAI.DFVSGames.Repetition.product_question_weight line 657
  72. theorem OAI.DFVSGames.Repetition.product_accepts_iff line 663
  73. theorem OAI.DFVSGames.Repetition.IsProjection.product line 670
  74. def OAI.DFVSGames.Repetition.productStrategy line 677
  75. theorem OAI.DFVSGames.Repetition.success_productStrategy line 681
  76. theorem OAI.DFVSGames.Repetition.mul_value_le_product_value line 698