OAI/Computability/PerfectCompleteness/Foundations/GoodAdviceEventsLemmas.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.GoodAdviceEvents.adapted_fiber_probability line 26
  2. theorem OAI.PerfectCompleteness.GoodAdviceEvents.adapted_uniform_fiber_probability line 36
  3. theorem OAI.PerfectCompleteness.GoodAdviceEvents.adapted_fiber_probability_zero line 49
  4. theorem OAI.PerfectCompleteness.GoodAdviceEvents.uniform_probability_eq_expect line 55
  5. theorem OAI.PerfectCompleteness.GoodAdviceEvents.product_probability line 66
  6. def OAI.PerfectCompleteness.GoodAdviceEvents.selectedColumn line 80
  7. def OAI.PerfectCompleteness.GoodAdviceEvents.selectedAgreement line 87
  8. def OAI.PerfectCompleteness.GoodAdviceEvents.J line 95
  9. def OAI.PerfectCompleteness.GoodAdviceEvents.I line 99
  10. def OAI.PerfectCompleteness.GoodAdviceEvents.law line 103
  11. theorem OAI.PerfectCompleteness.GoodAdviceEvents.I_implies_J line 110
  12. theorem OAI.PerfectCompleteness.GoodAdviceEvents.witness_agreement_probability line 121
  13. theorem OAI.PerfectCompleteness.GoodAdviceEvents.J_probability_fixed_row line 198
  14. theorem OAI.PerfectCompleteness.GoodAdviceEvents.I_probability_fixed_row line 242
  15. theorem OAI.PerfectCompleteness.GoodAdviceEvents.good_probability_eq_adviceMass line 287
  16. theorem OAI.PerfectCompleteness.GoodAdviceEvents.J_probability_ge line 296
  17. theorem OAI.PerfectCompleteness.GoodAdviceEvents.I_probability_ge line 314
  18. abbrev OAI.PerfectCompleteness.GoodAdviceFamily.Sample line 347
  19. def OAI.PerfectCompleteness.GoodAdviceFamily.law line 349
  20. def OAI.PerfectCompleteness.GoodAdviceFamily.J line 353
  21. def OAI.PerfectCompleteness.GoodAdviceFamily.I line 357
  22. theorem OAI.PerfectCompleteness.GoodAdviceFamily.J_probability_eq_mean line 362
  23. theorem OAI.PerfectCompleteness.GoodAdviceFamily.I_probability_eq_mean line 371
  24. theorem OAI.PerfectCompleteness.GoodAdviceFamily.J_probability_ge_mean_advice line 380
  25. theorem OAI.PerfectCompleteness.GoodAdviceFamily.I_probability_ge line 394
  26. theorem OAI.PerfectCompleteness.GoodAdviceFamily.J_probability_ge line 405