OAI/Probability/FreeIsing/Posterior/StoppingTimes.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.PosteriorStoppingTimes.rationalExit line 12
  2. theorem OAI.Problem367.PosteriorStoppingTimes.isStoppingTime_decision line 16
  3. theorem OAI.Problem367.PosteriorStoppingTimes.isStoppingTime_rationalExit line 41
  4. theorem OAI.Problem367.PosteriorStoppingTimes.isStoppingTime_rationalExit_rightCont line 51
  5. theorem OAI.Problem367.PosteriorStoppingTimes.rationalExit_mono line 58
  6. theorem OAI.Problem367.PosteriorStoppingTimes.le_rationalExit_of_bound line 67
  7. theorem OAI.Problem367.PosteriorStoppingTimes.exists_earlier_nnrat line 79
  8. theorem OAI.Problem367.PosteriorStoppingTimes.abs_le_of_le_rationalExit line 102
  9. abbrev OAI.Problem367.PosteriorStoppingTimes.threshold line 118
  10. def OAI.Problem367.PosteriorStoppingTimes.posteriorExit line 120
  11. theorem OAI.Problem367.PosteriorStoppingTimes.threshold_nonneg line 124
  12. theorem OAI.Problem367.PosteriorStoppingTimes.threshold_lt_one line 127
  13. theorem OAI.Problem367.PosteriorStoppingTimes.threshold_mono line 130
  14. theorem OAI.Problem367.PosteriorStoppingTimes.isStoppingTime_posteriorExit line 133
  15. theorem OAI.Problem367.PosteriorStoppingTimes.posteriorExit_mono line 139
  16. theorem OAI.Problem367.PosteriorStoppingTimes.posteriorExit_le_cap line 146
  17. theorem OAI.Problem367.PosteriorStoppingTimes.posteriorExit_ne_top line 149
  18. theorem OAI.Problem367.PosteriorStoppingTimes.abs_stoppedProcess_le line 153
  19. theorem OAI.Problem367.PosteriorStoppingTimes.eventually_lt_threshold line 168
  20. theorem OAI.Problem367.PosteriorStoppingTimes.eventually_le_posteriorExit line 172
  21. theorem OAI.Problem367.PosteriorStoppingTimes.tendsto_posteriorExit_top line 183
  22. theorem OAI.Problem367.PosteriorStoppingTimes.isLocalizingSequence_posteriorExit line 191
  23. theorem OAI.Problem367.PosteriorStoppingTimes.eventually_stoppedProcess_eq_on line 200
  24. theorem OAI.Problem367.PosteriorStoppingTimes.ae_all_eq_of_stopped_eq line 208
  25. theorem OAI.Problem367.PosteriorStoppingTimes.ae_all_add_eq_of_stopped_add_eq line 223
  26. theorem OAI.Problem367.PosteriorStoppingTimes.isLocalizingSequence_posteriorExit_rightCont line 233
  27. theorem OAI.Problem367.PosteriorStoppingTimes.isLocalizingSequence_of_field_bound line 242