OAI/Analysis/LipschitzHilbert/Estimates/RelativeMartingaleExits.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Relative exits for the finite scalar specialization of Zorin-Kranich, Bernoulli 26 (2020), Definition 2.1. The running radius is measured from the initial value; the terminal time is one step beyond the path in use.

  1. def OAI.LipschitzHilbert.runningOscillation line 14
  2. theorem OAI.LipschitzHilbert.runningOscillation_nonneg line 17
  3. theorem OAI.LipschitzHilbert.le_runningOscillation line 20
  4. theorem OAI.LipschitzHilbert.runningOscillation_le line 25
  5. theorem OAI.LipschitzHilbert.runningOscillation_mono line 32
  6. theorem OAI.LipschitzHilbert.runningOscillation_adapted line 36
  7. def OAI.LipschitzHilbert.relativeNextExit line 44
  8. theorem OAI.LipschitzHilbert.relativeNextExit_le line 48
  9. theorem OAI.LipschitzHilbert.relativeNextExit_isStopping line 51
  10. theorem OAI.LipschitzHilbert.relativeNextExit_ge line 60
  11. theorem OAI.LipschitzHilbert.relativeNextExit_before line 78
  12. theorem OAI.LipschitzHilbert.relativeNextExit_jump line 94
  13. def OAI.LipschitzHilbert.relativeExitTimes line 112
  14. theorem OAI.LipschitzHilbert.relativeExitTimes_le line 116
  15. theorem OAI.LipschitzHilbert.relativeExitTimes_isStopping line 122
  16. theorem OAI.LipschitzHilbert.relativeExitTimes_mono line 129
  17. theorem OAI.LipschitzHilbert.relativeExitTimes_min_le line 135
  18. theorem OAI.LipschitzHilbert.relativeExitTimes_terminal line 156