OAI/Computability/PerfectCompleteness/Reduction/OccurrenceGame.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PerfectCompleteness.OccurrenceGame line 15
  2. def OAI.PerfectCompleteness.OccurrenceGame.ofProjection line 27
  3. def OAI.PerfectCompleteness.OccurrenceGame.endpoints line 36
  4. def OAI.PerfectCompleteness.OccurrenceGame.wins line 39
  5. def OAI.PerfectCompleteness.OccurrenceGame.success line 43
  6. theorem OAI.PerfectCompleteness.OccurrenceGame.success_nonnegative line 47
  7. theorem OAI.PerfectCompleteness.OccurrenceGame.success_le_one line 51
  8. structure OAI.PerfectCompleteness.OccurrenceGame.EndpointPresentation line 55
  9. def OAI.PerfectCompleteness.OccurrenceGame.EndpointDetermined line 59
  10. def OAI.PerfectCompleteness.OccurrenceGame.chosenEndpointPredicate line 63
  11. def OAI.PerfectCompleteness.OccurrenceGame.presentationOfDetermined line 70
  12. theorem OAI.PerfectCompleteness.OccurrenceGame.EndpointPresentation.determined line 80
  13. def OAI.PerfectCompleteness.OccurrenceGame.toGame line 85
  14. theorem OAI.PerfectCompleteness.OccurrenceGame.toGame_success line 90
  15. def OAI.PerfectCompleteness.OccurrenceGame.repetition line 99
  16. def OAI.PerfectCompleteness.OccurrenceGame.EndpointPresentation.repetition line 109
  17. theorem OAI.PerfectCompleteness.OccurrenceGame.toGame_repetition_questions line 118
  18. theorem OAI.PerfectCompleteness.OccurrenceGame.toGame_repetition_success line 128
  19. def OAI.PerfectCompleteness.OccurrenceGame.value line 144
  20. theorem OAI.PerfectCompleteness.OccurrenceGame.success_le_value line 148
  21. theorem OAI.PerfectCompleteness.OccurrenceGame.value_le_iff line 153
  22. theorem OAI.PerfectCompleteness.OccurrenceGame.exists_optimal_strategy line 158
  23. theorem OAI.PerfectCompleteness.OccurrenceGame.value_nonnegative line 165
  24. theorem OAI.PerfectCompleteness.OccurrenceGame.value_le_one line 170
  25. theorem OAI.PerfectCompleteness.OccurrenceGame.randomized_success_le_value line 173
  26. theorem OAI.PerfectCompleteness.OccurrenceGame.toGame_value line 185
  27. theorem OAI.PerfectCompleteness.OccurrenceGame.toGame_repetition_value line 197