OAI/Computability/MinUncut/Games/OuterQuestions.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncut.Outer.SecondQuestion line 15
  2. def OAI.MinUncut.Outer.secondSlotCount line 17
  3. abbrev OAI.MinUncut.Outer.secondSlot line 20
  4. abbrev OAI.MinUncut.Outer.FirstAlphabet line 22
  5. abbrev OAI.MinUncut.Outer.FirstDirection line 23
  6. abbrev OAI.MinUncut.Outer.SecondAlphabet line 24
  7. def OAI.MinUncut.Outer.slotQuestion line 26
  8. def OAI.MinUncut.Outer.slotProjection line 29
  9. def OAI.MinUncut.Outer.secondQuestion line 35
  10. def OAI.MinUncut.Outer.projection line 38
  11. lemma OAI.MinUncut.Outer.projection_apply line 42
  12. def OAI.MinUncut.Outer.evaluatedTriple line 46
  13. def OAI.MinUncut.Outer.Satisfied line 47
  14. lemma OAI.MinUncut.Outer.evaluatedTriple_valid line 49
  15. def OAI.MinUncut.Outer.firstLabel line 53
  16. def OAI.MinUncut.Outer.secondSlotLabel line 57
  17. def OAI.MinUncut.Outer.secondLabel line 61
  18. lemma OAI.MinUncut.Outer.honest_slot line 64
  19. lemma OAI.MinUncut.Outer.honest_projection line 70
  20. def OAI.MinUncut.Outer.slotFunctional line 83
  21. lemma OAI.MinUncut.Outer.slotFunctional_add line 89
  22. lemma OAI.MinUncut.Outer.slotFunctional_smul line 95
  23. def OAI.MinUncut.Outer.directLinear line 103
  24. def OAI.MinUncut.Outer.directHint line 107
  25. lemma OAI.MinUncut.Outer.directHint_apply line 111
  26. lemma OAI.MinUncut.Outer.slotFunctional_project line 116
  27. lemma OAI.MinUncut.Outer.pulledHint_apply line 122
  28. lemma OAI.MinUncut.Outer.pulledHint_independent_active line 134
  29. def OAI.MinUncut.Outer.hintGenerator line 153
  30. def OAI.MinUncut.Outer.unpackFunctional line 170
  31. lemma OAI.MinUncut.Outer.oneSlotDual line 175
  32. lemma OAI.MinUncut.Outer.slotFunctional_unpack line 189
  33. lemma OAI.MinUncut.Outer.hintGenerator_surjective line 196
  34. lemma OAI.MinUncut.Outer.uniform_hintGenerator line 215
  35. def OAI.MinUncut.Outer.hintTupleGenerator line 219
  36. lemma OAI.MinUncut.Outer.hintTupleGenerator_surjective line 224
  37. lemma OAI.MinUncut.Outer.uniform_hintTupleGenerator line 230
  38. structure OAI.MinUncutGames.Foundations.Games.FiniteDistribution line 245
  39. def OAI.MinUncutGames.Foundations.Games.FiniteDistribution.expectation line 254
  40. def OAI.MinUncutGames.Foundations.Games.FiniteDistribution.probability line 257
  41. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.probability_nonnegative line 260
  42. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.probability_le_one line 268
  43. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.probability_true line 277
  44. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.probability_false line 281
  45. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.probability_mono line 285
  46. def OAI.MinUncutGames.Foundations.Games.FiniteDistribution.pushforward line 297
  47. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.probability_pushforward line 309
  48. def OAI.MinUncutGames.Foundations.Games.FiniteDistribution.transport line 321
  49. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.probability_transport line 326
  50. def OAI.MinUncutGames.Foundations.Games.FiniteDistribution.iid line 332
  51. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.probability_iid_all line 337
  52. abbrev OAI.MinUncutGames.Foundations.Games.Strategy line 356
  53. structure OAI.MinUncutGames.Foundations.Games.Game line 358
  54. def OAI.MinUncutGames.Foundations.Games.Game.wins line 368
  55. def OAI.MinUncutGames.Foundations.Games.Game.success line 372
  56. theorem OAI.MinUncutGames.Foundations.Games.Game.success_nonnegative line 375
  57. theorem OAI.MinUncutGames.Foundations.Games.Game.success_le_one line 379
  58. def OAI.MinUncutGames.Foundations.Games.Game.simulatedStrategy line 383
  59. theorem OAI.MinUncutGames.Foundations.Games.Game.success_le_of_localSimulation line 390
  60. def OAI.MinUncutGames.Foundations.Games.Game.tupleQuestionEquiv line 409
  61. def OAI.MinUncutGames.Foundations.Games.Game.repetition line 416
  62. def OAI.MinUncutGames.Foundations.Games.Game.repeatStrategy line 423
  63. theorem OAI.MinUncutGames.Foundations.Games.Game.success_repeatStrategy line 427
  64. theorem OAI.MinUncutGames.Foundations.Games.Game.repetition_question_weight line 435
  65. theorem OAI.MinUncutGames.Foundations.Games.Game.repetition_accepts_iff line 440
  66. def OAI.MinUncutGames.Foundations.Games.Game.coordinateWin line 447
  67. def OAI.MinUncutGames.Foundations.Games.Game.selectedWins line 453
  68. theorem OAI.MinUncutGames.Foundations.Games.Game.selectedWins_mono line 459
  69. theorem OAI.MinUncutGames.Foundations.Games.Game.selectedWins_empty line 470
  70. theorem OAI.MinUncutGames.Foundations.Games.Game.selectedWins_univ line 476
  71. def OAI.MinUncutGames.Foundations.Games.Game.value line 487
  72. theorem OAI.MinUncutGames.Foundations.Games.Game.success_le_value line 491
  73. theorem OAI.MinUncutGames.Foundations.Games.Game.value_le_iff line 496
  74. theorem OAI.MinUncutGames.Foundations.Games.Game.exists_optimal_strategy line 501
  75. theorem OAI.MinUncutGames.Foundations.Games.Game.value_nonnegative line 508
  76. theorem OAI.MinUncutGames.Foundations.Games.Game.value_le_one line 513
  77. theorem OAI.MinUncutGames.Foundations.Games.Game.randomized_success_le_value line 516
  78. theorem OAI.MinUncutGames.Foundations.Games.Game.success_repetition_zero line 529
  79. theorem OAI.MinUncutGames.Foundations.Games.Game.value_repetition_zero line 538
  80. theorem OAI.MinUncutGames.Foundations.Games.Game.pow_value_le_repetition_value line 544
  81. theorem OAI.MinUncutGames.Foundations.Games.Game.value_le_of_localSimulation line 550
  82. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.eq_of_weight_eq line 572
  83. def OAI.MinUncutGames.Foundations.Games.FiniteDistribution.table line 582
  84. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.expectation_table_eval line 593
  85. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.table_eval_pushforward line 621
  86. def OAI.MinUncutGames.Foundations.Games.FiniteDistribution.product line 635
  87. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.expectation_product line 644
  88. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.expectation_comm line 650
  89. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.expectation_congr line 663
  90. def OAI.MinUncutGames.Foundations.Games.Game.responseTableLaw line 676
  91. def OAI.MinUncutGames.Foundations.Games.Game.stochasticSuccess line 682
  92. theorem OAI.MinUncutGames.Foundations.Games.Game.success_eq_question_expectation line 691
  93. theorem OAI.MinUncutGames.Foundations.Games.Game.table_success_eq_stochastic line 698
  94. theorem OAI.MinUncutGames.Foundations.Games.Game.stochasticSuccess_le_value line 736
  95. theorem OAI.MinUncutGames.Foundations.Games.Game.exists_deterministic_ge_stochastic line 744