OAI/Computability/PerfectCompleteness/Foundations/HierarchicalRawPredictionLemmas.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.HierarchicalRawPrediction.Raw line 38
  2. abbrev OAI.PerfectCompleteness.HierarchicalRawPrediction.Visible line 39
  3. abbrev OAI.PerfectCompleteness.HierarchicalRawPrediction.rawArrays line 41
  4. abbrev OAI.PerfectCompleteness.HierarchicalRawPrediction.rawBackground line 44
  5. abbrev OAI.PerfectCompleteness.HierarchicalRawPrediction.rawMatrix line 48
  6. abbrev OAI.PerfectCompleteness.HierarchicalRawPrediction.visibleBackground line 51
  7. abbrev OAI.PerfectCompleteness.HierarchicalRawPrediction.known line 54
  8. abbrev OAI.PerfectCompleteness.HierarchicalRawPrediction.hidden line 57
  9. def OAI.PerfectCompleteness.HierarchicalRawPrediction.rawJ line 60
  10. def OAI.PerfectCompleteness.HierarchicalRawPrediction.rawPrediction line 68
  11. abbrev OAI.PerfectCompleteness.HierarchicalRawPrediction.VisibleGood line 74
  12. abbrev OAI.PerfectCompleteness.HierarchicalRawPrediction.tensorJ line 79
  13. abbrev OAI.PerfectCompleteness.HierarchicalRawPrediction.columnSpace line 85
  14. abbrev OAI.PerfectCompleteness.HierarchicalRawPrediction.target line 92
  15. abbrev OAI.PerfectCompleteness.HierarchicalRawPrediction.nativeCorrection line 101
  16. abbrev OAI.PerfectCompleteness.HierarchicalRawPrediction.visibleOffset line 108
  17. theorem OAI.PerfectCompleteness.HierarchicalRawPrediction.rawJ_eq_tensorJ line 115
  18. theorem OAI.PerfectCompleteness.HierarchicalRawPrediction.rawJ_iff_restriction line 128
  19. def OAI.PerfectCompleteness.HierarchicalRawPrediction.responseMatch line 147
  20. theorem OAI.PerfectCompleteness.HierarchicalRawPrediction.rawPrediction_eq line 160
  21. def OAI.PerfectCompleteness.HierarchicalRawPrediction.given line 200
  22. theorem OAI.PerfectCompleteness.HierarchicalRawPrediction.given_eq_jointEvent line 205
  23. theorem OAI.PerfectCompleteness.HierarchicalRawPrediction.selection_of_positive line 234
  24. theorem OAI.PerfectCompleteness.HierarchicalRawPrediction.conditional_prediction_eq line 265
  25. def OAI.PerfectCompleteness.HierarchicalRawMeeting.meetingProbability line 378
  26. theorem OAI.PerfectCompleteness.HierarchicalRawMeeting.meetingProbability_nonneg line 393
  27. theorem OAI.PerfectCompleteness.HierarchicalRawMeeting.meeting_probability_lower line 397