OAI/Computability/MinUncut/Games/Actual.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MinUncutGames.Reduction.ActualSource.Source line 12
  2. def OAI.MinUncutGames.Reduction.ActualSource.Source.sourceList line 18
  3. def OAI.MinUncutGames.Reduction.ActualSource.Source.ofList line 21
  4. theorem OAI.MinUncutGames.Reduction.ActualSource.Source.sourceList_ofList line 28
  5. theorem OAI.MinUncutGames.Reduction.ActualSource.Source.sourceList_length line 33
  6. theorem OAI.MinUncutGames.Reduction.ActualSource.Source.sourceList_nonempty line 36
  7. instance OAI.MinUncutGames.Reduction.ActualSource.sourceIndexNonempty line 44
  8. def OAI.MinUncutGames.Reduction.ActualSource.Source.satisfied line 47
  9. def OAI.MinUncutGames.Reduction.ActualSource.Source.failure line 50
  10. def OAI.MinUncutGames.Reduction.ActualSource.Source.DistinctNames line 53
  11. abbrev OAI.MinUncutGames.Reduction.ActualSource.Alphabet line 58
  12. abbrev OAI.MinUncutGames.Reduction.ActualSource.Ambient line 59
  13. def OAI.MinUncutGames.Reduction.ActualSource.alphabetEmbedding line 61
  14. theorem OAI.MinUncutGames.Reduction.ActualSource.alphabetEmbedding_apply line 64
  15. structure OAI.MinUncutGames.Reduction.ActualSource.SplitGadget line 67
  16. def OAI.MinUncutGames.Reduction.ActualSource.SplitGadget.stabilityError line 77
  17. def OAI.MinUncutGames.Reduction.ActualSource.SplitGadget.kernelError line 81
  18. theorem OAI.MinUncutGames.Reduction.ActualSource.SplitGadget.stabilityError_nonneg line 85
  19. theorem OAI.MinUncutGames.Reduction.ActualSource.SplitGadget.stabilityError_le_one line 91
  20. structure OAI.MinUncutGames.Reduction.Incidence.Triple line 106
  21. def OAI.MinUncutGames.Reduction.Incidence.parity line 112
  22. def OAI.MinUncutGames.Reduction.Incidence.matchingSlots line 114
  23. def OAI.MinUncutGames.Reduction.Incidence.acceptedSlots line 119
  24. def OAI.MinUncutGames.Reduction.Incidence.failedEquation line 122
  25. def OAI.MinUncutGames.Reduction.Incidence.bestResponse line 125
  26. theorem OAI.MinUncutGames.Reduction.Incidence.local_count_bound line 128
  27. theorem OAI.MinUncutGames.Reduction.Incidence.best_response_exact line 135
  28. structure OAI.MinUncutGames.Reduction.Incidence.Equation line 140
  29. inductive OAI.MinUncutGames.Reduction.Incidence.Slot line 146
  30. def OAI.MinUncutGames.Reduction.Incidence.nameAt line 152
  31. def OAI.MinUncutGames.Reduction.Incidence.bitAt line 157
  32. def OAI.MinUncutGames.Reduction.Incidence.questionPredicate line 162
  33. theorem OAI.MinUncutGames.Reduction.Incidence.question_predicate_at_slot line 169
  34. def OAI.MinUncutGames.Reduction.Incidence.bobTriple line 178
  35. def OAI.MinUncutGames.Reduction.Incidence.acceptedCount line 181
  36. def OAI.MinUncutGames.Reduction.Incidence.failureCount line 188
  37. theorem OAI.MinUncutGames.Reduction.Incidence.total_count_bound line 195
  38. def OAI.MinUncutGames.Reduction.Incidence.optimalAlice line 206
  39. theorem OAI.MinUncutGames.Reduction.Incidence.optimal_alice_exact line 210
  40. theorem OAI.MinUncutGames.Reduction.Incidence.fixed_bob_optimum line 221
  41. theorem OAI.MinUncutGames.Reduction.Incidence.soundness_191_over_192 line 235
  42. theorem OAI.MinUncutGames.Reduction.Incidence.game_soundness_191_over_192 line 242
  43. def OAI.MinUncutGames.Reduction.SourceIncidence.toIncidence line 259
  44. theorem OAI.MinUncutGames.Reduction.SourceIncidence.failedEquation_eq line 262
  45. theorem OAI.MinUncutGames.Reduction.SourceIncidence.failureCount_eq line 269
  46. def OAI.MinUncutGames.Reduction.SourceIncidence.occurrenceList line 280
  47. theorem OAI.MinUncutGames.Reduction.SourceIncidence.cloned_occurrence_gap line 283
  48. theorem OAI.MinUncutGames.Reduction.SourceIncidence.source_to_incidence_soundness line 302
  49. abbrev OAI.MinUncutGames.Reduction.FiniteSource.Name line 322
  50. def OAI.MinUncutGames.Reduction.FiniteSource.clonedSource line 324
  51. abbrev OAI.MinUncutGames.Reduction.FiniteSource.Occurrence line 326
  52. def OAI.MinUncutGames.Reduction.FiniteSource.occurrences line 328
  53. def OAI.MinUncutGames.Reduction.FiniteSource.rawEquation line 331
  54. def OAI.MinUncutGames.Reduction.FiniteSource.finiteName line 334
  55. def OAI.MinUncutGames.Reduction.FiniteSource.mapEquation line 337
  56. def OAI.MinUncutGames.Reduction.FiniteSource.equation line 340
  57. theorem OAI.MinUncutGames.Reduction.FiniteSource.satisfied_map line 343
  58. theorem OAI.MinUncutGames.Reduction.FiniteSource.mem_cart line 346
  59. theorem OAI.MinUncutGames.Reduction.FiniteSource.distinctTriple_bounds line 356
  60. theorem OAI.MinUncutGames.Reduction.FiniteSource.distinctTriples_nonempty line 363
  61. theorem OAI.MinUncutGames.Reduction.FiniteSource.cloned_member_properties line 368
  62. theorem OAI.MinUncutGames.Reduction.FiniteSource.raw_properties line 379
  63. theorem OAI.MinUncutGames.Reduction.FiniteSource.finiteName_injective_on line 388
  64. theorem OAI.MinUncutGames.Reduction.FiniteSource.names_distinct line 394
  65. theorem OAI.MinUncutGames.Reduction.FiniteSource.raw_map_occurrences line 403
  66. theorem OAI.MinUncutGames.Reduction.FiniteSource.occurrences_length line 407
  67. theorem OAI.MinUncutGames.Reduction.FiniteSource.clonedSource_nonempty line 411
  68. instance OAI.MinUncutGames.Reduction.FiniteSource.(instance at line 417) line 417
  69. theorem OAI.MinUncutGames.Reduction.FiniteSource.indexed_failure_count line 420
  70. theorem OAI.MinUncutGames.Reduction.FiniteSource.indexed_gap line 427
  71. theorem OAI.MinUncutGames.Reduction.FiniteSource.indexed_completeness_count line 436
  72. def OAI.MinUncutGames.Reduction.FiniteSource.incidenceEquation line 447
  73. theorem OAI.MinUncutGames.Reduction.FiniteSource.incidence_question_predicate line 450
  74. theorem OAI.MinUncutGames.Reduction.FiniteSource.incidence_failure_gap line 459
  75. theorem OAI.MinUncutGames.Reduction.FiniteSource.incidence_soundness line 469
  76. def OAI.MinUncutGames.Reduction.FiniteSource.nameEquiv line 477
  77. def OAI.MinUncutGames.Reduction.FiniteSource.cloned line 480
  78. theorem OAI.MinUncutGames.Reduction.FiniteSource.cloned_length line 486
  79. theorem OAI.MinUncutGames.Reduction.FiniteSource.cloned_distinct line 491
  80. theorem OAI.MinUncutGames.Reduction.FiniteSource.count_ofFn line 498
  81. theorem OAI.MinUncutGames.Reduction.FiniteSource.cloned_gap line 505
  82. theorem OAI.MinUncutGames.Reduction.FiniteSource.cloned_completeness_count line 520
  83. abbrev OAI.MinUncutGames.Soundness.IncidenceExtraction.Triple line 534
  84. def OAI.MinUncutGames.Soundness.IncidenceExtraction.xorTriple line 536
  85. structure OAI.MinUncutGames.Soundness.IncidenceExtraction.Incidence line 538
  86. def OAI.MinUncutGames.Soundness.IncidenceExtraction.Incidence.accepts line 542
  87. def OAI.MinUncutGames.Soundness.IncidenceExtraction.Incidence.namedAccepts line 547
  88. theorem OAI.MinUncutGames.Soundness.IncidenceExtraction.Incidence.accepts_implies_namedAccepts line 552
  89. theorem OAI.MinUncutGames.Soundness.IncidenceExtraction.Incidence.namedAccepts_iff_accepts line 558
  90. structure OAI.MinUncutGames.Soundness.IncidenceExtraction.FullPoint line 569
  91. def OAI.MinUncutGames.Soundness.IncidenceExtraction.FullPoint.valid line 573
  92. structure OAI.MinUncutGames.Soundness.IncidenceExtraction.PartnerPoint line 578
  93. def OAI.MinUncutGames.Soundness.IncidenceExtraction.AugmentedAccepts line 582
  94. def OAI.MinUncutGames.Soundness.IncidenceExtraction.RepeatedAccepts line 589
  95. theorem OAI.MinUncutGames.Soundness.IncidenceExtraction.augmented_accepts_implies_repeated_accepts line 595
  96. theorem OAI.MinUncutGames.Soundness.IncidenceExtraction.augmented_accepts_implies_named_repeated_accepts line 610
  97. structure OAI.MinUncutGames.Soundness.IncidenceExtraction.Game line 629
  98. structure OAI.MinUncutGames.Soundness.IncidenceExtraction.Strategies line 632
  99. def OAI.MinUncutGames.Soundness.IncidenceExtraction.Strategies.wins line 636
  100. structure OAI.MinUncutGames.Soundness.IncidenceExtraction.LocalSimulation line 640
  101. def OAI.MinUncutGames.Soundness.IncidenceExtraction.LocalSimulation.induced line 652
  102. theorem OAI.MinUncutGames.Soundness.IncidenceExtraction.LocalSimulation.induced_wins line 662
  103. theorem OAI.MinUncutGames.Soundness.IncidenceExtraction.LocalSimulation.seeded_induced_wins line 673