OAI/Computability/PerfectCompleteness/Reduction/ExactPreliminaryTarget.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.ExactPreliminaryTarget.namedGame line 45
  2. def OAI.PerfectCompleteness.ExactPreliminaryTarget.entry line 47
  3. theorem OAI.PerfectCompleteness.ExactPreliminaryTarget.entry_satisfied line 58
  4. def OAI.PerfectCompleteness.ExactPreliminaryTarget.construct line 65
  5. theorem OAI.PerfectCompleteness.ExactPreliminaryTarget.edge_count line 75
  6. theorem OAI.PerfectCompleteness.ExactPreliminaryTarget.leftVertices_eq_edges line 84
  7. theorem OAI.PerfectCompleteness.ExactPreliminaryTarget.rightVertices_eq_edges line 91
  8. theorem OAI.PerfectCompleteness.ExactPreliminaryTarget.rate_eq line 96
  9. theorem OAI.PerfectCompleteness.ExactPreliminaryTarget.value_eq line 111
  10. theorem OAI.PerfectCompleteness.ExactPreliminaryTarget.value_le line 139
  11. theorem OAI.PerfectCompleteness.ExactPreliminaryTarget.perfectlyComplete line 147
  12. theorem OAI.PerfectCompleteness.ExactPreliminaryTarget.encoding_length_le line 156