OAI/Computability/PerfectCompleteness/Foundations/HeterogeneousAdviceFamily.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.HeterogeneousAdviceFamily.Sample line 27
  2. def OAI.PerfectCompleteness.HeterogeneousAdviceFamily.law line 29
  3. def OAI.PerfectCompleteness.HeterogeneousAdviceFamily.J line 33
  4. def OAI.PerfectCompleteness.HeterogeneousAdviceFamily.I line 37
  5. theorem OAI.PerfectCompleteness.HeterogeneousAdviceFamily.J_probability_eq_mean line 43
  6. theorem OAI.PerfectCompleteness.HeterogeneousAdviceFamily.I_probability_eq_mean line 53
  7. theorem OAI.PerfectCompleteness.HeterogeneousAdviceFamily.div_pow_le line 61
  8. theorem OAI.PerfectCompleteness.HeterogeneousAdviceFamily.J_probability_ge_mean_advice line 68
  9. theorem OAI.PerfectCompleteness.HeterogeneousAdviceFamily.I_probability_ge line 87
  10. theorem OAI.PerfectCompleteness.HeterogeneousAdviceFamily.mean_adviceMass_ge line 100
  11. theorem OAI.PerfectCompleteness.HeterogeneousAdviceFamily.J_probability_ge line 136