OAI/Computability/DirectedFeedback/Probability/RepeatedGameBounds.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Soundness.RepeatedGameBounds.uniformAverage line 12
  2. def OAI.DFVSGames.Soundness.RepeatedGameBounds.zeroCount line 15
  3. theorem OAI.DFVSGames.Soundness.RepeatedGameBounds.power_zeroCount_eq_prod line 19
  4. theorem OAI.DFVSGames.Soundness.RepeatedGameBounds.sum_one_zero_weight line 25
  5. theorem OAI.DFVSGames.Soundness.RepeatedGameBounds.sum_power_zeroCount line 37
  6. theorem OAI.DFVSGames.Soundness.RepeatedGameBounds.uniformAverage_power_zeroCount line 45
  7. abbrev OAI.DFVSGames.Soundness.RepeatedGameBounds.BinaryCoefficient line 59
  8. theorem OAI.DFVSGames.Soundness.RepeatedGameBounds.card_binaryCoefficient line 61
  9. theorem OAI.DFVSGames.Soundness.RepeatedGameBounds.uniform_binary_coefficient_moment line 64
  10. theorem OAI.DFVSGames.Soundness.RepeatedGameBounds.uniformAverage_mono line 71
  11. theorem OAI.DFVSGames.Soundness.RepeatedGameBounds.uniformAverage_const line 77
  12. theorem OAI.DFVSGames.Soundness.RepeatedGameBounds.uniformAverage_prod line 82
  13. theorem OAI.DFVSGames.Soundness.RepeatedGameBounds.uniformAverage_equiv line 89
  14. theorem OAI.DFVSGames.Soundness.RepeatedGameBounds.uniformAverage_product_left line 95
  15. theorem OAI.DFVSGames.Soundness.RepeatedGameBounds.uniformAverage_coordinate_product line 101
  16. theorem OAI.DFVSGames.Soundness.RepeatedGameBounds.uniformAverage_power_zeroCount_indexed line 111
  17. def OAI.DFVSGames.Soundness.RepeatedGameBounds.splitRawCoefficients line 124
  18. theorem OAI.DFVSGames.Soundness.RepeatedGameBounds.zeroSet_card_eq_zeroCount line 145
  19. theorem OAI.DFVSGames.Soundness.RepeatedGameBounds.uniform_raw_coefficient_moment line 152
  20. theorem OAI.DFVSGames.Soundness.RepeatedGameBounds.uniform_binary_coefficient_upper line 166
  21. abbrev OAI.DFVSGames.Soundness.RepeatedGameBounds.Simulation.PredicateGame line 181
  22. abbrev OAI.DFVSGames.Soundness.RepeatedGameBounds.Simulation.PredicateStrategies line 182
  23. def OAI.DFVSGames.Soundness.RepeatedGameBounds.Simulation.predicateGame line 188
  24. def OAI.DFVSGames.Soundness.RepeatedGameBounds.Simulation.strategyPair line 191
  25. def OAI.DFVSGames.Soundness.RepeatedGameBounds.Simulation.weightedGame line 194
  26. def OAI.DFVSGames.Soundness.RepeatedGameBounds.Simulation.reconstructedGame line 199
  27. theorem OAI.DFVSGames.Soundness.RepeatedGameBounds.Simulation.reconstructedGame_success_le line 205
  28. theorem OAI.DFVSGames.Soundness.RepeatedGameBounds.Simulation.reconstructed_repetition_success_le line 222
  29. abbrev OAI.DFVSGames.Soundness.RepeatedGameBounds.ActualProjection.FirstAnswer line 236
  30. abbrev OAI.DFVSGames.Soundness.RepeatedGameBounds.ActualProjection.SecondAnswer line 237
  31. def OAI.DFVSGames.Soundness.RepeatedGameBounds.ActualProjection.project line 239
  32. def OAI.DFVSGames.Soundness.RepeatedGameBounds.ActualProjection.accepts line 244
  33. def OAI.DFVSGames.Soundness.RepeatedGameBounds.ActualProjection.predicateGame line 254
  34. theorem OAI.DFVSGames.Soundness.RepeatedGameBounds.ActualProjection.actual_partnerProjection_accepts line 260
  35. theorem OAI.DFVSGames.Soundness.RepeatedGameBounds.ActualProjection.accepts_implies_named_incidence line 277
  36. def OAI.DFVSGames.Soundness.ActualPointAnswers.sourceTau line 311
  37. def OAI.DFVSGames.Soundness.ActualPointAnswers.partnerTau line 312
  38. theorem OAI.DFVSGames.Soundness.ActualPointAnswers.tau_projection line 314
  39. def OAI.DFVSGames.Soundness.ActualPointAnswers.firstAnswer line 321
  40. def OAI.DFVSGames.Soundness.ActualPointAnswers.secondAnswer line 326
  41. theorem OAI.DFVSGames.Soundness.ActualPointAnswers.triple_eq_of_first_second_parity_inline_ActualPointAnswers line 331
  42. theorem OAI.DFVSGames.Soundness.ActualPointAnswers.secondAnswer_projection line 346
  43. def OAI.DFVSGames.Soundness.ActualPointAnswers.displayedRhs line 396
  44. theorem OAI.DFVSGames.Soundness.ActualPointAnswers.displayedRhs_full line 401
  45. theorem OAI.DFVSGames.Soundness.ActualPointAnswers.actual_accepts line 407
  46. def OAI.DFVSGames.Soundness.ActualInputRows.restrictedFirst line 450
  47. def OAI.DFVSGames.Soundness.ActualInputRows.firstMap line 456
  48. theorem OAI.DFVSGames.Soundness.ActualInputRows.firstMap_eq line 461
  49. def OAI.DFVSGames.Soundness.ActualInputRows.restrictedSecond line 470
  50. def OAI.DFVSGames.Soundness.ActualInputRows.secondMap line 476
  51. theorem OAI.DFVSGames.Soundness.ActualInputRows.secondMap_eq line 481
  52. theorem OAI.DFVSGames.Soundness.ActualInputRows.firstMap_actual line 490
  53. theorem OAI.DFVSGames.Soundness.ActualInputRows.secondMap_actual line 509
  54. abbrev OAI.DFVSGames.Clean.AnswerBridge.FirstInput line 542
  55. abbrev OAI.DFVSGames.Clean.AnswerBridge.SecondInput line 543
  56. abbrev OAI.DFVSGames.Clean.AnswerBridge.SourceAnswer line 545
  57. abbrev OAI.DFVSGames.Clean.AnswerBridge.TargetAnswer line 546
  58. abbrev OAI.DFVSGames.Clean.AnswerBridge.PointStrategies line 548
  59. theorem OAI.DFVSGames.Clean.AnswerBridge.firstAnswer_eq_embed line 553
  60. def OAI.DFVSGames.Clean.AnswerBridge.toOuterStrategy line 569
  61. theorem OAI.DFVSGames.Clean.AnswerBridge.toOuterStrategy_wins line 580
  62. def OAI.DFVSGames.Clean.AnswerBridge.finiteCoordinates line 599
  63. def OAI.DFVSGames.Clean.AnswerBridge.bitsCoordinatesEquiv line 603
  64. def OAI.DFVSGames.Clean.AnswerBridge.encodeCoefficients line 607
  65. def OAI.DFVSGames.Clean.AnswerBridge.coefficientsEquiv line 612
  66. theorem OAI.DFVSGames.Clean.AnswerBridge.uniform_encoded_coefficients line 616
  67. theorem OAI.DFVSGames.Clean.AnswerBridge.encoded_map_coefficients line 623
  68. theorem OAI.DFVSGames.Clean.AnswerBridge.zeroSet_encodeCoefficients line 628
  69. def OAI.DFVSGames.Clean.AnswerBridge.rowPointStrategies line 642
  70. theorem OAI.DFVSGames.Clean.AnswerBridge.rowPointStrategies_first_actual line 652
  71. theorem OAI.DFVSGames.Clean.AnswerBridge.rowPointStrategies_second_actual line 672
  72. def OAI.DFVSGames.Clean.AnswerBridge.defaultTargetAnswer line 693
  73. def OAI.DFVSGames.Clean.AnswerBridge.extendSupportedPolicy line 696
  74. theorem OAI.DFVSGames.Clean.AnswerBridge.extendSupportedPolicy_apply line 703
  75. def OAI.DFVSGames.Soundness.ConditionalIncidences.coordinateReindex line 717
  76. theorem OAI.DFVSGames.Soundness.ConditionalIncidences.raw_conditional_incidence_reindex line 727
  77. theorem OAI.DFVSGames.Soundness.ConditionalIncidences.raw_conditional_event_reindex_real line 747