OAI/Computability/PerfectCompleteness/Reduction/HierarchicalFixedAdviceFamilyLemmas.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.HierarchicalFixedAdviceFamily.inverse_factor_eq_q line 23
  2. theorem OAI.PerfectCompleteness.HierarchicalFixedAdviceFamily.coarse_error_small line 30
  3. theorem OAI.PerfectCompleteness.HierarchicalFixedAdviceFamily.rows_positive line 68
  4. def OAI.PerfectCompleteness.HierarchicalFixedAdviceFamily.predictionDifference line 72
  5. theorem OAI.PerfectCompleteness.HierarchicalFixedAdviceFamily.mean_agreement_ge line 88
  6. theorem OAI.PerfectCompleteness.HierarchicalFixedAdviceFamily.prediction_difference line 103
  7. def OAI.PerfectCompleteness.PreliminaryStrategy.observe line 149
  8. abbrev OAI.PerfectCompleteness.PreliminaryStrategy.Strategy line 163
  9. def OAI.PerfectCompleteness.PreliminaryStrategy.extend line 169
  10. theorem OAI.PerfectCompleteness.PreliminaryStrategy.observe_extend_iff line 176
  11. theorem OAI.PerfectCompleteness.PreliminaryStrategy.wins_eq_observe line 190
  12. theorem OAI.PerfectCompleteness.PreliminaryStrategy.success_eq_shared_candidate_mean line 209