OAI/Computability/PerfectCompleteness/Reduction/PreliminaryOutputLemmas.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.PreliminaryOutput.value line 19
  2. theorem OAI.PerfectCompleteness.PreliminaryOutput.exists_target line 29
  3. theorem OAI.PerfectCompleteness.PreliminaryOutput.exists_target_size_bound line 66
  4. theorem OAI.PerfectCompleteness.FixedPreliminaryGame.depth_pos line 128
  5. theorem OAI.PerfectCompleteness.FixedPreliminaryGame.rows_pos line 130
  6. def OAI.PerfectCompleteness.FixedPreliminaryGame.game line 133
  7. abbrev OAI.PerfectCompleteness.FixedPreliminaryGame.Strategy line 138
  8. def OAI.PerfectCompleteness.FixedPreliminaryGame.value line 142
  9. theorem OAI.PerfectCompleteness.FixedPreliminaryGame.completeness line 147
  10. theorem OAI.PerfectCompleteness.FixedPreliminaryGame.exists_level_pair line 162
  11. theorem OAI.PerfectCompleteness.FixedPreliminaryValue.exists_optimal_strategy line 190
  12. theorem OAI.PerfectCompleteness.FixedPreliminaryValue.value_lt_of_strategy_lt line 201
  13. theorem OAI.PerfectCompleteness.FixedPreliminaryValue.value_le_of_no_large_strategy line 208
  14. theorem OAI.PerfectCompleteness.PreliminaryPairReserve.exists_pair line 227