OAI/Computability/BinPacking/PCP/OccurrenceGame.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.BinPackingCompleteness.OccurrenceGame line 12
  2. def OAI.BinPackingCompleteness.OccurrenceGame.ofProjection line 24
  3. def OAI.BinPackingCompleteness.OccurrenceGame.endpoints line 33
  4. def OAI.BinPackingCompleteness.OccurrenceGame.wins line 36
  5. def OAI.BinPackingCompleteness.OccurrenceGame.success line 40
  6. theorem OAI.BinPackingCompleteness.OccurrenceGame.success_nonnegative line 44
  7. theorem OAI.BinPackingCompleteness.OccurrenceGame.success_le_one line 48
  8. structure OAI.BinPackingCompleteness.OccurrenceGame.EndpointPresentation line 52
  9. def OAI.BinPackingCompleteness.OccurrenceGame.EndpointDetermined line 56
  10. def OAI.BinPackingCompleteness.OccurrenceGame.chosenEndpointPredicate line 60
  11. def OAI.BinPackingCompleteness.OccurrenceGame.presentationOfDetermined line 67
  12. theorem OAI.BinPackingCompleteness.OccurrenceGame.EndpointPresentation.determined line 77
  13. def OAI.BinPackingCompleteness.OccurrenceGame.toGame line 82
  14. theorem OAI.BinPackingCompleteness.OccurrenceGame.toGame_success line 87
  15. def OAI.BinPackingCompleteness.OccurrenceGame.repetition line 96
  16. def OAI.BinPackingCompleteness.OccurrenceGame.EndpointPresentation.repetition line 106
  17. theorem OAI.BinPackingCompleteness.OccurrenceGame.toGame_repetition_questions line 115
  18. theorem OAI.BinPackingCompleteness.OccurrenceGame.toGame_repetition_success line 125
  19. def OAI.BinPackingCompleteness.OccurrenceGame.value line 140
  20. theorem OAI.BinPackingCompleteness.OccurrenceGame.success_le_value line 144
  21. theorem OAI.BinPackingCompleteness.OccurrenceGame.value_le_iff line 149
  22. theorem OAI.BinPackingCompleteness.OccurrenceGame.exists_optimal_strategy line 154
  23. theorem OAI.BinPackingCompleteness.OccurrenceGame.value_nonnegative line 161
  24. theorem OAI.BinPackingCompleteness.OccurrenceGame.value_le_one line 166
  25. theorem OAI.BinPackingCompleteness.OccurrenceGame.randomized_success_le_value line 169
  26. theorem OAI.BinPackingCompleteness.OccurrenceGame.toGame_value line 181
  27. theorem OAI.BinPackingCompleteness.OccurrenceGame.toGame_repetition_value line 193