OAI/Computability/PerfectCompleteness/Foundations/HierarchicalProjectedPredictionLemmas.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.HierarchicalProjectedPrediction.rawJ line 39
  2. def OAI.PerfectCompleteness.HierarchicalProjectedPrediction.rawPrediction line 46
  3. theorem OAI.PerfectCompleteness.HierarchicalProjectedPrediction.J_rawRead line 55
  4. theorem OAI.PerfectCompleteness.HierarchicalProjectedPrediction.prediction_rawRead line 76
  5. theorem OAI.PerfectCompleteness.HierarchicalProjectedPrediction.J_probability line 95
  6. theorem OAI.PerfectCompleteness.HierarchicalProjectedPrediction.prediction_probability line 132
  7. abbrev OAI.PerfectCompleteness.HierarchicalProjectedAverage.RawSample line 203
  8. def OAI.PerfectCompleteness.HierarchicalProjectedAverage.meetingProbability line 207
  9. def OAI.PerfectCompleteness.HierarchicalProjectedAverage.expectedMeeting line 213
  10. def OAI.PerfectCompleteness.HierarchicalProjectedAverage.predictionDifference line 218
  11. theorem OAI.PerfectCompleteness.HierarchicalProjectedAverage.expectedMeeting_eq_fibers line 226
  12. theorem OAI.PerfectCompleteness.HierarchicalProjectedAverage.predictionDifference_eq_fibers line 239
  13. theorem OAI.PerfectCompleteness.HierarchicalProjectedAverage.expectedMeeting_ge_prediction_difference line 264
  14. theorem OAI.PerfectCompleteness.HierarchicalProjectedAverage.factor_mul_b_eq_gamma line 281
  15. theorem OAI.PerfectCompleteness.HierarchicalProjectedAverage.expectedMeeting_ge_gamma line 325
  16. def OAI.PerfectCompleteness.HierarchicalProjectedOuterAverage.factor line 368
  17. theorem OAI.PerfectCompleteness.HierarchicalProjectedOuterAverage.factor_nonneg line 372
  18. theorem OAI.PerfectCompleteness.HierarchicalProjectedOuterAverage.factor_mul_b_eq_gamma line 376
  19. abbrev OAI.PerfectCompleteness.HierarchicalProjectedOuterAverage.experiment line 397
  20. def OAI.PerfectCompleteness.HierarchicalProjectedOuterAverage.expectedMeeting line 405
  21. def OAI.PerfectCompleteness.HierarchicalProjectedOuterAverage.predictionDifference line 410
  22. theorem OAI.PerfectCompleteness.HierarchicalProjectedOuterAverage.predictionDifference_eq_mean line 418
  23. theorem OAI.PerfectCompleteness.HierarchicalProjectedOuterAverage.expectedMeeting_ge_prediction_difference line 430
  24. theorem OAI.PerfectCompleteness.HierarchicalProjectedOuterAverage.expectedMeeting_ge_gamma_of_mean line 463
  25. def OAI.PerfectCompleteness.HierarchicalWholePrediction.rawJ line 528
  26. def OAI.PerfectCompleteness.HierarchicalWholePrediction.rawPrediction line 534
  27. theorem OAI.PerfectCompleteness.HierarchicalWholePrediction.J_rawRead line 541
  28. theorem OAI.PerfectCompleteness.HierarchicalWholePrediction.prediction_rawRead line 561
  29. theorem OAI.PerfectCompleteness.HierarchicalWholePrediction.J_probability line 578
  30. theorem OAI.PerfectCompleteness.HierarchicalWholePrediction.prediction_probability line 613
  31. abbrev OAI.PerfectCompleteness.HierarchicalWholeAverage.RawSample line 681
  32. def OAI.PerfectCompleteness.HierarchicalWholeAverage.meetingProbability line 685
  33. def OAI.PerfectCompleteness.HierarchicalWholeAverage.expectedMeeting line 690
  34. def OAI.PerfectCompleteness.HierarchicalWholeAverage.predictionDifference line 695
  35. theorem OAI.PerfectCompleteness.HierarchicalWholeAverage.expectedMeeting_eq_fibers line 703
  36. theorem OAI.PerfectCompleteness.HierarchicalWholeAverage.predictionDifference_eq_fibers line 716
  37. theorem OAI.PerfectCompleteness.HierarchicalWholeAverage.expectedMeeting_ge_prediction_difference line 741
  38. theorem OAI.PerfectCompleteness.HierarchicalWholeAverage.factor_mul_b_eq_gamma line 757
  39. theorem OAI.PerfectCompleteness.HierarchicalWholeAverage.expectedMeeting_ge_gamma line 799