OAI/Probability/FreeIsing/Posterior/ContinuousObservationHistory.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.ContinuousObservationHistory.stoppedPath line 15
  2. theorem OAI.Problem367.ContinuousObservationHistory.stoppedPath_apply line 19
  3. theorem OAI.Problem367.ContinuousObservationHistory.measurable_stoppedPath line 22
  4. theorem OAI.Problem367.ContinuousObservationHistory.stoppedPath_stoppedPath line 27
  5. def OAI.Problem367.ContinuousObservationHistory.stoppedArray line 34
  6. theorem OAI.Problem367.ContinuousObservationHistory.measurable_stoppedArray line 37
  7. theorem OAI.Problem367.ContinuousObservationHistory.stoppedArray_stoppedArray line 41
  8. theorem OAI.Problem367.ContinuousObservationHistory.monotone_stoppedArray_comap line 46
  9. theorem OAI.Problem367.ContinuousObservationHistory.measurable_stoppedArray_of_eval line 54
  10. theorem OAI.Problem367.ContinuousObservationHistory.measurable_past_of_stoppedArray line 64
  11. theorem OAI.Problem367.ContinuousObservationHistory.stoppedArray_comap_eq_past line 77
  12. theorem OAI.Problem367.ContinuousObservationHistory.stoppedArray_comap_eq_natural line 94
  13. def OAI.Problem367.ContinuousObservationHistory.joinedFiltration line 102
  14. theorem OAI.Problem367.ContinuousObservationHistory.commonNoise_martingale line 107