OAI/Computability/PerfectCompleteness/Foundations/DependentPredictionDifferenceLemmas.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.DependentPredictionDifference.Sample line 17
  2. abbrev OAI.PerfectCompleteness.DependentPredictionDifference.Observation line 19
  3. def OAI.PerfectCompleteness.DependentPredictionDifference.law line 24
  4. def OAI.PerfectCompleteness.DependentPredictionDifference.observe line 29
  5. theorem OAI.PerfectCompleteness.DependentPredictionDifference.original_usefulness_predicts line 32
  6. theorem OAI.PerfectCompleteness.DependentPredictionDifference.of_original_usefulness line 52
  7. def OAI.PerfectCompleteness.LegalEnumeration.reindex line 99
  8. def OAI.PerfectCompleteness.LegalEnumeration.strategies line 106
  9. theorem OAI.PerfectCompleteness.LegalEnumeration.reindex_wins line 109
  10. theorem OAI.PerfectCompleteness.LegalEnumeration.reindex_success line 123
  11. theorem OAI.PerfectCompleteness.LegalEnumeration.reindex_fiber_card line 135
  12. theorem OAI.PerfectCompleteness.LegalEnumeration.reindex_at_most_two line 154
  13. theorem OAI.PerfectCompleteness.LegalEnumeration.reindex_value line 170
  14. abbrev OAI.PerfectCompleteness.LegalEnumeration.NumberedLabels line 186
  15. def OAI.PerfectCompleteness.LegalEnumeration.numberedLabelEquiv line 189
  16. def OAI.PerfectCompleteness.LegalEnumeration.numbered line 193
  17. theorem OAI.PerfectCompleteness.LegalEnumeration.numbered_at_most_two line 200
  18. theorem OAI.PerfectCompleteness.LegalEnumeration.numbered_value line 209
  19. theorem OAI.PerfectCompleteness.SigmaObservation.eq_of_probability_eq line 225
  20. theorem OAI.PerfectCompleteness.SigmaObservation.pushforward_fiber line 233