OAI/Analysis/LipschitzHilbert/Estimates/MartingaleGeometricTail.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Iterating the first-crossing contraction gives a geometric tail with constants independent of the number of time steps.

  1. theorem OAI.LipschitzHilbert.martingale_geometric_tail line 17
  2. theorem OAI.LipschitzHilbert.martingale_terminal_geometric_tail line 37