OAI/Analysis/LipschitzHilbert/Estimates/MartingaleExitTimes.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Actual successive exits from a fixed-radius ball around the previous stopped value. All times stay inside the prescribed finite horizon.

  1. def OAI.LipschitzHilbert.nextMartingaleExit line 14
  2. theorem OAI.LipschitzHilbert.nextMartingaleExit_le line 19
  3. theorem OAI.LipschitzHilbert.nextMartingaleExit_isStopping line 22
  4. theorem OAI.LipschitzHilbert.nextMartingaleExit_ge line 32
  5. theorem OAI.LipschitzHilbert.nextMartingaleExit_before line 49
  6. def OAI.LipschitzHilbert.martingaleExitTimes line 61
  7. theorem OAI.LipschitzHilbert.martingaleExitTimes_le line 66
  8. theorem OAI.LipschitzHilbert.martingaleExitTimes_isStopping line 72
  9. theorem OAI.LipschitzHilbert.martingaleExitTimes_mono line 80
  10. theorem OAI.LipschitzHilbert.nextMartingaleExit_jump line 85
  11. theorem OAI.LipschitzHilbert.martingaleExitTimes_min_le line 101
  12. theorem OAI.LipschitzHilbert.martingaleExitTimes_terminal line 121
  13. theorem OAI.LipschitzHilbert.martingaleExitTimes_jump_energy line 126