OAI/Probability/FreeIsing/Posterior/CompensatorStopping.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.PosteriorCompensatorStopping.jointExit line 14
  2. theorem OAI.Problem367.PosteriorCompensatorStopping.jointExit_le_posteriorExit line 18
  3. theorem OAI.Problem367.PosteriorCompensatorStopping.jointExit_le_cap line 21
  4. theorem OAI.Problem367.PosteriorCompensatorStopping.jointExit_ne_top line 25
  5. theorem OAI.Problem367.PosteriorCompensatorStopping.jointExit_mono line 29
  6. theorem OAI.Problem367.PosteriorCompensatorStopping.isStoppingTime_jointExit line 35
  7. theorem OAI.Problem367.PosteriorCompensatorStopping.abs_stoppedProcess_le_of_le_exit line 41
  8. theorem OAI.Problem367.PosteriorCompensatorStopping.abs_stopped_posterior_le line 56
  9. theorem OAI.Problem367.PosteriorCompensatorStopping.abs_stopped_compensator_le line 63
  10. theorem OAI.Problem367.PosteriorCompensatorStopping.eventually_le_compensatorExit line 69
  11. theorem OAI.Problem367.PosteriorCompensatorStopping.eventually_le_jointExit line 81
  12. theorem OAI.Problem367.PosteriorCompensatorStopping.tendsto_jointExit_top line 89
  13. theorem OAI.Problem367.PosteriorCompensatorStopping.isLocalizingSequence_jointExit line 98
  14. theorem OAI.Problem367.PosteriorCompensatorStopping.isLocalizingSequence_jointExit_rightCont line 109
  15. theorem OAI.Problem367.PosteriorCompensatorStopping.eventually_stoppedProcess_eq_on line 119
  16. theorem OAI.Problem367.PosteriorCompensatorStopping.ae_all_eq_of_stopped_eq line 128