OAI/Computability/PerfectCompleteness/Reduction/CanonicalGameLemmas.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PerfectCompleteness.CanonicalGame.BlockFamily line 22
  2. abbrev OAI.PerfectCompleteness.CanonicalGame.RightOutput line 33
  3. def OAI.PerfectCompleteness.CanonicalGame.rightPresentation line 36
  4. def OAI.PerfectCompleteness.CanonicalGame.leftKey line 39
  5. def OAI.PerfectCompleteness.CanonicalGame.rightKey line 41
  6. abbrev OAI.PerfectCompleteness.CanonicalGame.LeftVertex line 43
  7. abbrev OAI.PerfectCompleteness.CanonicalGame.RightVertex line 44
  8. def OAI.PerfectCompleteness.CanonicalGame.leftAt line 46
  9. def OAI.PerfectCompleteness.CanonicalGame.rightAt line 47
  10. abbrev OAI.PerfectCompleteness.CanonicalGame.LeftLabel line 49
  11. abbrev OAI.PerfectCompleteness.CanonicalGame.RightLabel line 50
  12. instance OAI.PerfectCompleteness.CanonicalGame.leftVertex_finite line 52
  13. instance OAI.PerfectCompleteness.CanonicalGame.rightVertex_finite line 57
  14. instance OAI.PerfectCompleteness.CanonicalGame.leftLabel_nonempty line 62
  15. instance OAI.PerfectCompleteness.CanonicalGame.rightLabel_nonempty line 66
  16. def OAI.PerfectCompleteness.CanonicalGame.edge line 70
  17. theorem OAI.PerfectCompleteness.CanonicalGame.edge_at_most_two line 75
  18. def OAI.PerfectCompleteness.CanonicalGame.game line 82
  19. def OAI.PerfectCompleteness.CanonicalGame.leftAmbientVertex line 89
  20. def OAI.PerfectCompleteness.CanonicalGame.rightAmbientVertex line 95
  21. def OAI.PerfectCompleteness.CanonicalGame.leftStrategy line 99
  22. def OAI.PerfectCompleteness.CanonicalGame.rightStrategy line 103
  23. theorem OAI.PerfectCompleteness.CanonicalGame.leftStrategy_at line 108
  24. theorem OAI.PerfectCompleteness.CanonicalGame.rightStrategy_at line 116
  25. def OAI.PerfectCompleteness.CanonicalGame.satisfyingStrategy line 124
  26. theorem OAI.PerfectCompleteness.CanonicalGame.edge_strategy line 129
  27. theorem OAI.PerfectCompleteness.CanonicalGame.success_satisfyingStrategy line 149
  28. theorem OAI.PerfectCompleteness.CanonicalGameStrategy.left_right_disjoint line 179
  29. def OAI.PerfectCompleteness.CanonicalGameStrategy.support line 186
  30. def OAI.PerfectCompleteness.CanonicalGameStrategy.onSupport line 188
  31. def OAI.PerfectCompleteness.CanonicalGameStrategy.extend line 193
  32. theorem OAI.PerfectCompleteness.CanonicalGameStrategy.extend_left_val line 196
  33. theorem OAI.PerfectCompleteness.CanonicalGameStrategy.extend_right_val line 208
  34. theorem OAI.PerfectCompleteness.CanonicalGameStrategy.label_extend_left line 223
  35. theorem OAI.PerfectCompleteness.CanonicalGameStrategy.label_extend_right line 230
  36. theorem OAI.PerfectCompleteness.CanonicalGameStrategy.response_extend_left line 237
  37. theorem OAI.PerfectCompleteness.CanonicalGameStrategy.response_extend_right line 245
  38. theorem OAI.PerfectCompleteness.CanonicalGameStrategy.accepts_extend_iff line 254
  39. abbrev OAI.PerfectCompleteness.CompletionRounding.SeededOccurrences line 281
  40. theorem OAI.PerfectCompleteness.CompletionRounding.seeded_weights_total line 283
  41. def OAI.PerfectCompleteness.CompletionRounding.enumeratedWeights line 297
  42. theorem OAI.PerfectCompleteness.CompletionRounding.probability_one_forall_of_positive line 307
  43. abbrev OAI.PerfectCompleteness.CompletionRounding.CompletedOccurrence line 329
  44. def OAI.PerfectCompleteness.CompletionRounding.enumeration line 332
  45. def OAI.PerfectCompleteness.CompletionRounding.weights line 336
  46. def OAI.PerfectCompleteness.CompletionRounding.entries line 340
  47. theorem OAI.PerfectCompleteness.CompletionRounding.entries_satisfied line 348
  48. theorem OAI.PerfectCompleteness.CompletionRounding.weight_cast line 356
  49. theorem OAI.PerfectCompleteness.CompletionRounding.weightedSuccess_eq_completed line 365
  50. def OAI.PerfectCompleteness.CompletionRounding.output line 390
  51. theorem OAI.PerfectCompleteness.CompletionRounding.support_card line 394
  52. theorem OAI.PerfectCompleteness.CompletionRounding.output_edge_count line 398
  53. theorem OAI.PerfectCompleteness.CompletionRounding.output_edge_count_le line 403
  54. theorem OAI.PerfectCompleteness.CompletionRounding.output_value_le line 411
  55. theorem OAI.PerfectCompleteness.CompletionRounding.output_value_le_of_residual_bound line 427
  56. theorem OAI.PerfectCompleteness.CompletionRounding.output_value_eq_one line 442
  57. theorem OAI.PerfectCompleteness.CompletionProbability.exists_completion_sampler_bounded line 479
  58. theorem OAI.PerfectCompleteness.CompletionSoundness.LegalProjectionGame.exists_completionFamily_bounded line 531