OAI/Computability/PerfectCompleteness/Foundations/HierarchicalProjectedRawAverage.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.HierarchicalProjectedRawAverage.event_mass_le_expectation line 19
  2. abbrev OAI.PerfectCompleteness.HierarchicalProjectedRawAverage.Raw line 48
  3. abbrev OAI.PerfectCompleteness.HierarchicalProjectedRawAverage.Visible line 51
  4. def OAI.PerfectCompleteness.HierarchicalProjectedRawAverage.law line 54
  5. abbrev OAI.PerfectCompleteness.HierarchicalProjectedRawAverage.J line 60
  6. abbrev OAI.PerfectCompleteness.HierarchicalProjectedRawAverage.prediction line 64
  7. def OAI.PerfectCompleteness.HierarchicalProjectedRawAverage.goodRecord line 68
  8. def OAI.PerfectCompleteness.HierarchicalProjectedRawAverage.goodEvent line 77
  9. def OAI.PerfectCompleteness.HierarchicalProjectedRawAverage.factor line 84
  10. theorem OAI.PerfectCompleteness.HierarchicalProjectedRawAverage.factor_nonneg line 90
  11. abbrev OAI.PerfectCompleteness.HierarchicalProjectedRawAverage.meetingProbability line 94
  12. def OAI.PerfectCompleteness.HierarchicalProjectedRawAverage.expectedMeeting line 98
  13. theorem OAI.PerfectCompleteness.HierarchicalProjectedRawAverage.meeting_lower_of_goodRecord line 104
  14. theorem OAI.PerfectCompleteness.HierarchicalProjectedRawAverage.expectedMeeting_ge_good_mass line 173
  15. theorem OAI.PerfectCompleteness.HierarchicalProjectedRawAverage.J_and_prediction line 188
  16. theorem OAI.PerfectCompleteness.HierarchicalProjectedRawAverage.prediction_difference_le_good_mass line 197
  17. theorem OAI.PerfectCompleteness.HierarchicalProjectedRawAverage.expectedMeeting_ge_prediction_difference line 217