OAI/Computability/PerfectCompleteness/Foundations/HierarchicalRawAverage.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.HierarchicalRawAverage.event_mass_le_expectation line 19
  2. abbrev OAI.PerfectCompleteness.HierarchicalRawAverage.Raw line 47
  3. abbrev OAI.PerfectCompleteness.HierarchicalRawAverage.Visible line 50
  4. def OAI.PerfectCompleteness.HierarchicalRawAverage.law line 53
  5. abbrev OAI.PerfectCompleteness.HierarchicalRawAverage.J line 59
  6. abbrev OAI.PerfectCompleteness.HierarchicalRawAverage.prediction line 63
  7. def OAI.PerfectCompleteness.HierarchicalRawAverage.goodRecord line 67
  8. def OAI.PerfectCompleteness.HierarchicalRawAverage.goodEvent line 76
  9. def OAI.PerfectCompleteness.HierarchicalRawAverage.factor line 83
  10. theorem OAI.PerfectCompleteness.HierarchicalRawAverage.factor_nonneg line 89
  11. abbrev OAI.PerfectCompleteness.HierarchicalRawAverage.meetingProbability line 93
  12. def OAI.PerfectCompleteness.HierarchicalRawAverage.expectedMeeting line 97
  13. theorem OAI.PerfectCompleteness.HierarchicalRawAverage.meeting_lower_of_goodRecord line 103
  14. theorem OAI.PerfectCompleteness.HierarchicalRawAverage.expectedMeeting_ge_good_mass line 172
  15. theorem OAI.PerfectCompleteness.HierarchicalRawAverage.J_and_prediction line 187
  16. theorem OAI.PerfectCompleteness.HierarchicalRawAverage.prediction_difference_le_good_mass line 196
  17. theorem OAI.PerfectCompleteness.HierarchicalRawAverage.expectedMeeting_ge_prediction_difference line 216