OAI/Analysis/LipschitzHilbert/Estimates/MartingaleLocalMaximal.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Restriction and time shift for a martingale, and the local weak-L1 maximal estimate used in the dyadic John--Nirenberg stopping argument.

  1. def OAI.LipschitzHilbert.timeShiftFiltration line 19
  2. theorem OAI.LipschitzHilbert.martingale_timeShift line 25
  3. theorem OAI.LipschitzHilbert.martingale_restrict_initial line 30
  4. theorem OAI.LipschitzHilbert.martingale_abs line 39
  5. theorem OAI.LipschitzHilbert.martingale_maximal_L1 line 47
  6. theorem OAI.LipschitzHilbert.martingale_local_maximal_L1 line 77